Theorem sbcrexg 2366

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

Assertion

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

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

Proof of Theorem sbcrexg

Step	Hyp	Ref	Expression
1		dfsbcq 2288	. 2 |- (z = A -> ([z / x]E.y e. B ph <-> [A / x]E.y e. B ph))
2		dfsbcq 2288	. . 3 |- (z = A -> ([z / x]ph <-> [A / x]ph))
3	2	rexbidv 1958	. 2 |- (z = A -> (E.y e. B [z / x]ph <-> E.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	hbrex 1983	. . 3 |- (E.y e. B [z / x]ph -> A.xE.y e. B [z / x]ph)
7		sbequ12 1383	. . . 4 |- (x = z -> (ph <-> [z / x]ph))
8	7	rexbidv 1958	. . 3 |- (x = z -> (E.y e. B ph <-> E.y e. B [z / x]ph))
9	6, 8	sbie 1403	. 2 |- ([z / x]E.y e. B ph <-> E.y e. B [z / x]ph)
10	1, 3, 9	vtoclbg 2180	1 |- (A e. C -> ([A / x]E.y e. B ph <-> E.y e. B [A / x]ph))

Syntax hints:   -> wi 3   <-> wb 162   = wceq 1136   e. wcel 1138  [wsbc 1372  E.wrex 1940

This theorem is referenced by:  ac6sfi 5320

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-rex 1944  df-v 2127  df-sbc 2287

Copyright terms: Public domain