Theorem rabxfrd 3842

Description: Class builder membership after substituting an expression A (containing y) for x in the class expression ch.

Hypotheses

Ref	Expression
rabxfrd.1	|- (z e. B -> A.y z e. B)
rabxfrd.2	|- (z e. C -> A.y z e. C)
rabxfrd.3	|- ((ph /\ y e. D) -> A e. D)
rabxfrd.4	|- (x = A -> (ps <-> ch))
rabxfrd.5	|- (y = B -> A = C)

Assertion

Ref	Expression
rabxfrd	|- ((ph /\ B e. D) -> (C e. {x e. D | ps} <-> B e. {y e. D | ch}))

Distinct variable groups:   x,A   z,B   z,C   x,y,z,D   ph,y   ps,y,z   ch,x,z

Proof of Theorem rabxfrd

Step	Hyp	Ref	Expression
1		rabxfrd.3	. . . . . . . . . . 11 |- ((ph /\ y e. D) -> A e. D)
2	1	ex 402	. . . . . . . . . 10 |- (ph -> (y e. D -> A e. D))
3		ibibr 651	. . . . . . . . . 10 |- ((y e. D -> A e. D) <-> (y e. D -> (A e. D <-> y e. D)))
4	2, 3	sylib 215	. . . . . . . . 9 |- (ph -> (y e. D -> (A e. D <-> y e. D)))
5	4	imp 377	. . . . . . . 8 |- ((ph /\ y e. D) -> (A e. D <-> y e. D))
6	5	anbi1d 679	. . . . . . 7 |- ((ph /\ y e. D) -> ((A e. D /\ ch) <-> (y e. D /\ ch)))
7		rabxfrd.4	. . . . . . . 8 |- (x = A -> (ps <-> ch))
8	7	elrab 2414	. . . . . . 7 |- (A e. {x e. D | ps} <-> (A e. D /\ ch))
9		rabid 2253	. . . . . . 7 |- (y e. {y e. D | ch} <-> (y e. D /\ ch))
10	6, 8, 9	3bitr4g 614	. . . . . 6 |- ((ph /\ y e. D) -> (A e. {x e. D | ps} <-> y e. {y e. D | ch}))
11	10	rabbidva 2286	. . . . 5 |- (ph -> {y e. D | A e. {x e. D | ps}} = {y e. D | y e. {y e. D | ch}})
12	11	eleq2d 1964	. . . 4 |- (ph -> (B e. {y e. D | A e. {x e. D | ps}} <-> B e. {y e. D | y e. {y e. D | ch}}))
13		rabxfrd.1	. . . . 5 |- (z e. B -> A.y z e. B)
14		ax-17 1317	. . . . 5 |- (z e. D -> A.y z e. D)
15		rabxfrd.2	. . . . . 6 |- (z e. C -> A.y z e. C)
16		ax-17 1317	. . . . . 6 |- (z e. {x e. D | ps} -> A.y z e. {x e. D | ps})
17	15, 16	hbel 1996	. . . . 5 |- (C e. {x e. D | ps} -> A.y C e. {x e. D | ps})
18		rabxfrd.5	. . . . . 6 |- (y = B -> A = C)
19	18	eleq1d 1963	. . . . 5 |- (y = B -> (A e. {x e. D | ps} <-> C e. {x e. D | ps}))
20	13, 14, 17, 19	elrabf 2413	. . . 4 |- (B e. {y e. D | A e. {x e. D | ps}} <-> (B e. D /\ C e. {x e. D | ps}))
21		hbrab1 2257	. . . . . 6 |- (z e. {y e. D | ch} -> A.y z e. {y e. D | ch})
22	13, 21	hbel 1996	. . . . 5 |- (B e. {y e. D | ch} -> A.y B e. {y e. D | ch})
23		eleq1 1957	. . . . 5 |- (y = B -> (y e. {y e. D | ch} <-> B e. {y e. D | ch}))
24	13, 14, 22, 23	elrabf 2413	. . . 4 |- (B e. {y e. D | y e. {y e. D | ch}} <-> (B e. D /\ B e. {y e. D | ch}))
25	12, 20, 24	3bitr3g 613	. . 3 |- (ph -> ((B e. D /\ C e. {x e. D | ps}) <-> (B e. D /\ B e. {y e. D | ch})))
26		pm5.32 706	. . 3 |- ((B e. D -> (C e. {x e. D | ps} <-> B e. {y e. D | ch})) <-> ((B e. D /\ C e. {x e. D | ps}) <-> (B e. D /\ B e. {y e. D | ch})))
27	25, 26	sylibr 217	. 2 |- (ph -> (B e. D -> (C e. {x e. D | ps} <-> B e. {y e. D | ch})))
28	27	imp 377	1 |- ((ph /\ B e. D) -> (C e. {x e. D | ps} <-> B e. {y e. D | ch}))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  {crab 2108

This theorem is referenced by:  rabxfr 3843  riotaxfrd 5581

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-rab 2112  df-v 2294

Copyright terms: Public domain