Theorem sbcralg 2364

Description: Interchange class substitution and restricted quantifier. (The proof was shortened by Andrew Salmon, 29-Jun-2011.)

Assertion

Ref	Expression
sbcralg	|- (A e. C -> ([A / x]A.y e. B ph <-> A.y e. B [A / x]ph))

Distinct variable groups:   y,A   x,B   x,y

Proof of Theorem sbcralg

Step	Hyp	Ref	Expression
1		dfsbcq 2288	. 2 |- (z = A -> ([z / x]A.y e. B ph <-> [A / x]A.y e. B ph))
2		dfsbcq 2288	. . 3 |- (z = A -> ([z / x]ph <-> [A / x]ph))
3	2	ralbidv 1957	. 2 |- (z = A -> (A.y e. B [z / x]ph <-> A.y e. B [A / x]ph))
4		ax-17 1155	. . . 4 |- (y e. B -> A.x y e. B)
5		hbs1 1560	. . . 4 |- ([z / x]ph -> A.x[z / x]ph)
6	4, 5	hbral 1980	. . 3 |- (A.y e. B [z / x]ph -> A.xA.y e. B [z / x]ph)
7		sbequ12 1383	. . . 4 |- (x = z -> (ph <-> [z / x]ph))
8	7	ralbidv 1957	. . 3 |- (x = z -> (A.y e. B ph <-> A.y e. B [z / x]ph))
9	6, 8	sbie 1403	. 2 |- ([z / x]A.y e. B ph <-> A.y e. B [z / x]ph)
10	1, 3, 9	vtoclbg 2180	1 |- (A e. C -> ([A / x]A.y e. B ph <-> A.y e. B [A / x]ph))

Syntax hints:   -> wi 3   <-> wb 162   = wceq 1136   e. wcel 1138  [wsbc 1372  A.wral 1939

This theorem is referenced by:  r19.12sn 2915  ra4sbc2 5638  csbfsum 8082  bnj82 13002  bnj92 13008  ra4sbc2VD 16338

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1142  ax-gen 1143  ax-8 1144  ax-9 1145  ax-10 1146  ax-11 1147  ax-12 1148  ax-17 1155  ax-4 1157  ax-5o 1159  ax-6o 1162  ax-9o 1319  ax-10o 1338  ax-16 1418  ax-11o 1426  ax-ext 1702

This theorem depends on definitions:  df-bi 163  df-or 240  df-an 241  df-ex 1165  df-sb 1374  df-clab 1709  df-cleq 1714  df-clel 1717  df-ral 1943  df-v 2127  df-sbc 2287

Copyright terms: Public domain