Metamath Proof Explorer


Theorem rabxfrd

Description: Membership in a restricted class abstraction after substituting an expression A (containing y ) for x in the formula defining the class abstraction. (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 ( ( 𝜑𝐵𝐷 ) → ( 𝐶 ∈ { 𝑥𝐷𝜓 } ↔ 𝐵 ∈ { 𝑦𝐷𝜒 } ) )