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 𝐹 = ( 𝑥𝐷 ↦ { 𝑦𝐵𝜑 } )
elmptrab.s1 ( ( 𝑥 = 𝑋𝑦 = 𝑌 ) → ( 𝜑𝜓 ) )
elmptrab.s2 ( 𝑥 = 𝑋𝐵 = 𝐶 )
elmptrab.ex ( 𝑥𝐷𝐵𝑉 )
Assertion elmptrab ( 𝑌 ∈ ( 𝐹𝑋 ) ↔ ( 𝑋𝐷𝑌𝐶𝜓 ) )

Proof

Step Hyp Ref Expression
1 elmptrab.f 𝐹 = ( 𝑥𝐷 ↦ { 𝑦𝐵𝜑 } )
2 elmptrab.s1 ( ( 𝑥 = 𝑋𝑦 = 𝑌 ) → ( 𝜑𝜓 ) )
3 elmptrab.s2 ( 𝑥 = 𝑋𝐵 = 𝐶 )
4 elmptrab.ex ( 𝑥𝐷𝐵𝑉 )
5 1 mptrcl ( 𝑌 ∈ ( 𝐹𝑋 ) → 𝑋𝐷 )
6 simp1 ( ( 𝑋𝐷𝑌𝐶𝜓 ) → 𝑋𝐷 )
7 csbeq1 ( 𝑧 = 𝑋 𝑧 / 𝑥 𝐵 = 𝑋 / 𝑥 𝐵 )
8 dfsbcq ( 𝑧 = 𝑋 → ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑[ 𝑋 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) )
9 7 8 rabeqbidv ( 𝑧 = 𝑋 → { 𝑤 𝑧 / 𝑥 𝐵[ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } = { 𝑤 𝑋 / 𝑥 𝐵[ 𝑋 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } )
10 nfcv 𝑧 { 𝑦𝐵𝜑 }
11 nfsbc1v 𝑥 [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑
12 nfcsb1v 𝑥 𝑧 / 𝑥 𝐵
13 11 12 nfrabw 𝑥 { 𝑤 𝑧 / 𝑥 𝐵[ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 }
14 csbeq1a ( 𝑥 = 𝑧𝐵 = 𝑧 / 𝑥 𝐵 )
15 sbceq1a ( 𝑥 = 𝑧 → ( 𝜑[ 𝑧 / 𝑥 ] 𝜑 ) )
16 14 15 rabeqbidv ( 𝑥 = 𝑧 → { 𝑦𝐵𝜑 } = { 𝑦 𝑧 / 𝑥 𝐵[ 𝑧 / 𝑥 ] 𝜑 } )
17 nfcv 𝑤 𝑧 / 𝑥 𝐵
18 nfcv 𝑦 𝑧 / 𝑥 𝐵
19 nfcv 𝑦 𝑧
20 nfsbc1v 𝑦 [ 𝑤 / 𝑦 ] 𝜑
21 19 20 nfsbcw 𝑦 [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑
22 nfv 𝑤 [ 𝑧 / 𝑥 ] 𝜑
23 sbccom ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑[ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑 )
24 sbceq1a ( 𝑦 = 𝑤 → ( [ 𝑧 / 𝑥 ] 𝜑[ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑 ) )
25 24 equcoms ( 𝑤 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑[ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑 ) )
26 23 25 bitr4id ( 𝑤 = 𝑦 → ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑[ 𝑧 / 𝑥 ] 𝜑 ) )
27 17 18 21 22 26 cbvrabw { 𝑤 𝑧 / 𝑥 𝐵[ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } = { 𝑦 𝑧 / 𝑥 𝐵[ 𝑧 / 𝑥 ] 𝜑 }
28 16 27 eqtr4di ( 𝑥 = 𝑧 → { 𝑦𝐵𝜑 } = { 𝑤 𝑧 / 𝑥 𝐵[ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } )
29 10 13 28 cbvmpt ( 𝑥𝐷 ↦ { 𝑦𝐵𝜑 } ) = ( 𝑧𝐷 ↦ { 𝑤 𝑧 / 𝑥 𝐵[ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } )
30 1 29 eqtri 𝐹 = ( 𝑧𝐷 ↦ { 𝑤 𝑧 / 𝑥 𝐵[ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } )
31 nfv 𝑥 𝑧𝐷
32 12 nfel1 𝑥 𝑧 / 𝑥 𝐵𝑉
33 31 32 nfim 𝑥 ( 𝑧𝐷 𝑧 / 𝑥 𝐵𝑉 )
34 eleq1w ( 𝑥 = 𝑧 → ( 𝑥𝐷𝑧𝐷 ) )
35 14 eleq1d ( 𝑥 = 𝑧 → ( 𝐵𝑉 𝑧 / 𝑥 𝐵𝑉 ) )
36 34 35 imbi12d ( 𝑥 = 𝑧 → ( ( 𝑥𝐷𝐵𝑉 ) ↔ ( 𝑧𝐷 𝑧 / 𝑥 𝐵𝑉 ) ) )
37 33 36 4 chvarfv ( 𝑧𝐷 𝑧 / 𝑥 𝐵𝑉 )
38 rabexg ( 𝑧 / 𝑥 𝐵𝑉 → { 𝑤 𝑧 / 𝑥 𝐵[ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } ∈ V )
39 37 38 syl ( 𝑧𝐷 → { 𝑤 𝑧 / 𝑥 𝐵[ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } ∈ V )
40 9 30 39 fvmpt3 ( 𝑋𝐷 → ( 𝐹𝑋 ) = { 𝑤 𝑋 / 𝑥 𝐵[ 𝑋 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } )
41 40 eleq2d ( 𝑋𝐷 → ( 𝑌 ∈ ( 𝐹𝑋 ) ↔ 𝑌 ∈ { 𝑤 𝑋 / 𝑥 𝐵[ 𝑋 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } ) )
42 dfsbcq ( 𝑤 = 𝑌 → ( [ 𝑤 / 𝑦 ] 𝜑[ 𝑌 / 𝑦 ] 𝜑 ) )
43 42 sbcbidv ( 𝑤 = 𝑌 → ( [ 𝑋 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑[ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) )
44 43 elrab ( 𝑌 ∈ { 𝑤 𝑋 / 𝑥 𝐵[ 𝑋 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } ↔ ( 𝑌 𝑋 / 𝑥 𝐵[ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) )
45 44 a1i ( 𝑋𝐷 → ( 𝑌 ∈ { 𝑤 𝑋 / 𝑥 𝐵[ 𝑋 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } ↔ ( 𝑌 𝑋 / 𝑥 𝐵[ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) ) )
46 nfcvd ( 𝑋𝐷 𝑥 𝐶 )
47 46 3 csbiegf ( 𝑋𝐷 𝑋 / 𝑥 𝐵 = 𝐶 )
48 47 eleq2d ( 𝑋𝐷 → ( 𝑌 𝑋 / 𝑥 𝐵𝑌𝐶 ) )
49 48 anbi1d ( 𝑋𝐷 → ( ( 𝑌 𝑋 / 𝑥 𝐵[ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) ↔ ( 𝑌𝐶[ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) ) )
50 nfv 𝑥 𝜓
51 nfv 𝑦 𝜓
52 nfv 𝑥 𝑌𝐶
53 50 51 52 2 sbc2iegf ( ( 𝑋𝐷𝑌𝐶 ) → ( [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑𝜓 ) )
54 53 pm5.32da ( 𝑋𝐷 → ( ( 𝑌𝐶[ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) ↔ ( 𝑌𝐶𝜓 ) ) )
55 45 49 54 3bitrd ( 𝑋𝐷 → ( 𝑌 ∈ { 𝑤 𝑋 / 𝑥 𝐵[ 𝑋 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } ↔ ( 𝑌𝐶𝜓 ) ) )
56 3anass ( ( 𝑋𝐷𝑌𝐶𝜓 ) ↔ ( 𝑋𝐷 ∧ ( 𝑌𝐶𝜓 ) ) )
57 56 baibr ( 𝑋𝐷 → ( ( 𝑌𝐶𝜓 ) ↔ ( 𝑋𝐷𝑌𝐶𝜓 ) ) )
58 41 55 57 3bitrd ( 𝑋𝐷 → ( 𝑌 ∈ ( 𝐹𝑋 ) ↔ ( 𝑋𝐷𝑌𝐶𝜓 ) ) )
59 5 6 58 pm5.21nii ( 𝑌 ∈ ( 𝐹𝑋 ) ↔ ( 𝑋𝐷𝑌𝐶𝜓 ) )