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	⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐶 ∈ { 𝑥 ∈ 𝐷 ∣ 𝜓 } ↔ 𝐵 ∈ { 𝑦 ∈ 𝐷 ∣ 𝜒 } ) )