Metamath Proof Explorer


Theorem elmptrab

Description: Membership in a one-parameter class of sets. (Contributed by Stefan O'Rear, 28-Jul-2015)

Ref Expression
Hypotheses elmptrab.f F = x D y B | φ
elmptrab.s1 x = X y = Y φ ψ
elmptrab.s2 x = X B = C
elmptrab.ex x D B V
Assertion elmptrab Y F X X D Y C ψ

Proof

Step Hyp Ref Expression
1 elmptrab.f F = x D y B | φ
2 elmptrab.s1 x = X y = Y φ ψ
3 elmptrab.s2 x = X B = C
4 elmptrab.ex x D B V
5 1 mptrcl Y F X X D
6 simp1 X D Y C ψ X D
7 csbeq1 z = X z / x B = X / x B
8 dfsbcq z = X [˙z / x]˙ [˙w / y]˙ φ [˙X / x]˙ [˙w / y]˙ φ
9 7 8 rabeqbidv z = X w z / x B | [˙z / x]˙ [˙w / y]˙ φ = w X / x B | [˙X / x]˙ [˙w / y]˙ φ
10 nfcv _ z y B | φ
11 nfsbc1v x [˙z / x]˙ [˙w / y]˙ φ
12 nfcsb1v _ x z / x B
13 11 12 nfrabw _ x w z / x B | [˙z / x]˙ [˙w / y]˙ φ
14 csbeq1a x = z B = z / x B
15 sbceq1a x = z φ [˙z / x]˙ φ
16 14 15 rabeqbidv x = z y B | φ = y z / x B | [˙z / x]˙ φ
17 nfcv _ w z / x B
18 nfcv _ y z / x B
19 nfcv _ y z
20 nfsbc1v y [˙w / y]˙ φ
21 19 20 nfsbcw y [˙z / x]˙ [˙w / y]˙ φ
22 nfv w [˙z / x]˙ φ
23 sbccom [˙z / x]˙ [˙w / y]˙ φ [˙w / y]˙ [˙z / x]˙ φ
24 sbceq1a y = w [˙z / x]˙ φ [˙w / y]˙ [˙z / x]˙ φ
25 24 equcoms w = y [˙z / x]˙ φ [˙w / y]˙ [˙z / x]˙ φ
26 23 25 bitr4id w = y [˙z / x]˙ [˙w / y]˙ φ [˙z / x]˙ φ
27 17 18 21 22 26 cbvrabw w z / x B | [˙z / x]˙ [˙w / y]˙ φ = y z / x B | [˙z / x]˙ φ
28 16 27 eqtr4di x = z y B | φ = w z / x B | [˙z / x]˙ [˙w / y]˙ φ
29 10 13 28 cbvmpt x D y B | φ = z D w z / x B | [˙z / x]˙ [˙w / y]˙ φ
30 1 29 eqtri F = z D w z / x B | [˙z / x]˙ [˙w / y]˙ φ
31 nfv x z D
32 12 nfel1 x z / x B V
33 31 32 nfim x z D z / x B V
34 eleq1w x = z x D z D
35 14 eleq1d x = z B V z / x B V
36 34 35 imbi12d x = z x D B V z D z / x B V
37 33 36 4 chvarfv z D z / x B V
38 rabexg z / x B V w z / x B | [˙z / x]˙ [˙w / y]˙ φ V
39 37 38 syl z D w z / x B | [˙z / x]˙ [˙w / y]˙ φ V
40 9 30 39 fvmpt3 X D F X = w X / x B | [˙X / x]˙ [˙w / y]˙ φ
41 40 eleq2d X D Y F X Y w X / x B | [˙X / x]˙ [˙w / y]˙ φ
42 dfsbcq w = Y [˙w / y]˙ φ [˙Y / y]˙ φ
43 42 sbcbidv w = Y [˙X / x]˙ [˙w / y]˙ φ [˙X / x]˙ [˙Y / y]˙ φ
44 43 elrab Y w X / x B | [˙X / x]˙ [˙w / y]˙ φ Y X / x B [˙X / x]˙ [˙Y / y]˙ φ
45 44 a1i X D Y w X / x B | [˙X / x]˙ [˙w / y]˙ φ Y X / x B [˙X / x]˙ [˙Y / y]˙ φ
46 nfcvd X D _ x C
47 46 3 csbiegf X D X / x B = C
48 47 eleq2d X D Y X / x B Y C
49 48 anbi1d X D Y X / x B [˙X / x]˙ [˙Y / y]˙ φ Y C [˙X / x]˙ [˙Y / y]˙ φ
50 nfv x ψ
51 nfv y ψ
52 nfv x Y C
53 50 51 52 2 sbc2iegf X D Y C [˙X / x]˙ [˙Y / y]˙ φ ψ
54 53 pm5.32da X D Y C [˙X / x]˙ [˙Y / y]˙ φ Y C ψ
55 45 49 54 3bitrd X D Y w X / x B | [˙X / x]˙ [˙w / y]˙ φ Y C ψ
56 3anass X D Y C ψ X D Y C ψ
57 56 baibr X D Y C ψ X D Y C ψ
58 41 55 57 3bitrd X D Y F X X D Y C ψ
59 5 6 58 pm5.21nii Y F X X D Y C ψ