Metamath Proof Explorer

Theorem rabxfrd

Description: Class builder membership after substituting an expression A (containing y ) for x in the class expression ch . (Contributed by NM, 16-Jan-2012)

Ref Expression
Hypotheses rabxfrd.1 ⊢ Ⅎ 𝑦 𝐵
rabxfrd.2 ⊢ Ⅎ 𝑦 𝐶
rabxfrd.3 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝐴 ∈ 𝐷 )
rabxfrd.4 ⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜒 ) )
rabxfrd.5 ⊢ ( 𝑦 = 𝐵 → 𝐴 = 𝐶 )
Assertion rabxfrd ( ( 𝜑 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐶 ∈ { 𝑥 ∈ 𝐷 ∣ 𝜓 } ↔ 𝐵 ∈ { 𝑦 ∈ 𝐷 ∣ 𝜒 } ) )

Proof

Step Hyp Ref Expression
1 rabxfrd.1 ⊢ Ⅎ 𝑦 𝐵
2 rabxfrd.2 ⊢ Ⅎ 𝑦 𝐶
3 rabxfrd.3 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝐴 ∈ 𝐷 )
4 rabxfrd.4 ⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜒 ) )
5 rabxfrd.5 ⊢ ( 𝑦 = 𝐵 → 𝐴 = 𝐶 )
6 3 ex ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 → 𝐴 ∈ 𝐷 ) )
7 ibibr ⊢ ( ( 𝑦 ∈ 𝐷 → 𝐴 ∈ 𝐷 ) ↔ ( 𝑦 ∈ 𝐷 → ( 𝐴 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷 ) ) )
8 6 7 sylib ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 → ( 𝐴 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷 ) ) )
9 8 imp ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝐴 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷 ) )
10 9 anbi1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝐴 ∈ 𝐷 ∧ 𝜒 ) ↔ ( 𝑦 ∈ 𝐷 ∧ 𝜒 ) ) )
11 4 elrab ⊢ ( 𝐴 ∈ { 𝑥 ∈ 𝐷 ∣ 𝜓 } ↔ ( 𝐴 ∈ 𝐷 ∧ 𝜒 ) )
12 rabid ⊢ ( 𝑦 ∈ { 𝑦 ∈ 𝐷 ∣ 𝜒 } ↔ ( 𝑦 ∈ 𝐷 ∧ 𝜒 ) )
13 10 11 12 3bitr4g ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝐴 ∈ { 𝑥 ∈ 𝐷 ∣ 𝜓 } ↔ 𝑦 ∈ { 𝑦 ∈ 𝐷 ∣ 𝜒 } ) )
14 13 rabbidva ⊢ ( 𝜑 → { 𝑦 ∈ 𝐷 ∣ 𝐴 ∈ { 𝑥 ∈ 𝐷 ∣ 𝜓 } } = { 𝑦 ∈ 𝐷 ∣ 𝑦 ∈ { 𝑦 ∈ 𝐷 ∣ 𝜒 } } )
15 14 eleq2d ⊢ ( 𝜑 → ( 𝐵 ∈ { 𝑦 ∈ 𝐷 ∣ 𝐴 ∈ { 𝑥 ∈ 𝐷 ∣ 𝜓 } } ↔ 𝐵 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∈ { 𝑦 ∈ 𝐷 ∣ 𝜒 } } ) )
16 nfcv ⊢ Ⅎ 𝑦 𝐷
17 2 nfel1 ⊢ Ⅎ 𝑦 𝐶 ∈ { 𝑥 ∈ 𝐷 ∣ 𝜓 }
18 5 eleq1d ⊢ ( 𝑦 = 𝐵 → ( 𝐴 ∈ { 𝑥 ∈ 𝐷 ∣ 𝜓 } ↔ 𝐶 ∈ { 𝑥 ∈ 𝐷 ∣ 𝜓 } ) )
19 1 16 17 18 elrabf ⊢ ( 𝐵 ∈ { 𝑦 ∈ 𝐷 ∣ 𝐴 ∈ { 𝑥 ∈ 𝐷 ∣ 𝜓 } } ↔ ( 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ { 𝑥 ∈ 𝐷 ∣ 𝜓 } ) )
20 nfrab1 ⊢ Ⅎ 𝑦 { 𝑦 ∈ 𝐷 ∣ 𝜒 }
21 1 20 nfel ⊢ Ⅎ 𝑦 𝐵 ∈ { 𝑦 ∈ 𝐷 ∣ 𝜒 }
22 eleq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 ∈ { 𝑦 ∈ 𝐷 ∣ 𝜒 } ↔ 𝐵 ∈ { 𝑦 ∈ 𝐷 ∣ 𝜒 } ) )
23 1 16 21 22 elrabf ⊢ ( 𝐵 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∈ { 𝑦 ∈ 𝐷 ∣ 𝜒 } } ↔ ( 𝐵 ∈ 𝐷 ∧ 𝐵 ∈ { 𝑦 ∈ 𝐷 ∣ 𝜒 } ) )
24 15 19 23 3bitr3g ⊢ ( 𝜑 → ( ( 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ { 𝑥 ∈ 𝐷 ∣ 𝜓 } ) ↔ ( 𝐵 ∈ 𝐷 ∧ 𝐵 ∈ { 𝑦 ∈ 𝐷 ∣ 𝜒 } ) ) )
25 pm5.32 ⊢ ( ( 𝐵 ∈ 𝐷 → ( 𝐶 ∈ { 𝑥 ∈ 𝐷 ∣ 𝜓 } ↔ 𝐵 ∈ { 𝑦 ∈ 𝐷 ∣ 𝜒 } ) ) ↔ ( ( 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ { 𝑥 ∈ 𝐷 ∣ 𝜓 } ) ↔ ( 𝐵 ∈ 𝐷 ∧ 𝐵 ∈ { 𝑦 ∈ 𝐷 ∣ 𝜒 } ) ) )
26 24 25 sylibr ⊢ ( 𝜑 → ( 𝐵 ∈ 𝐷 → ( 𝐶 ∈ { 𝑥 ∈ 𝐷 ∣ 𝜓 } ↔ 𝐵 ∈ { 𝑦 ∈ 𝐷 ∣ 𝜒 } ) ) )
27 26 imp ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐶 ∈ { 𝑥 ∈ 𝐷 ∣ 𝜓 } ↔ 𝐵 ∈ { 𝑦 ∈ 𝐷 ∣ 𝜒 } ) )