Theorem rabxfr

Description: Membership in a restricted class abstraction after substituting an expression A (containing y ) for x in the the formula defining the class abstraction. (Contributed by NM, 10-Jun-2005)

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

Proof

Step	Hyp	Ref	Expression
1		rabxfr.1	⊢ Ⅎ 𝑦 𝐵
2		rabxfr.2	⊢ Ⅎ 𝑦 𝐶
3		rabxfr.3	⊢ ( 𝑦 ∈ 𝐷 → 𝐴 ∈ 𝐷 )
4		rabxfr.4	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
5		rabxfr.5	⊢ ( 𝑦 = 𝐵 → 𝐴 = 𝐶 )
6		tru	⊢ ⊤
7	3	adantl	⊢ ( ( ⊤ ∧ 𝑦 ∈ 𝐷 ) → 𝐴 ∈ 𝐷 )
8	1 2 7 4 5	rabxfrd	⊢ ( ( ⊤ ∧ 𝐵 ∈ 𝐷 ) → ( 𝐶 ∈ { 𝑥 ∈ 𝐷 ∣ 𝜑 } ↔ 𝐵 ∈ { 𝑦 ∈ 𝐷 ∣ 𝜓 } ) )
9	6 8	mpan	⊢ ( 𝐵 ∈ 𝐷 → ( 𝐶 ∈ { 𝑥 ∈ 𝐷 ∣ 𝜑 } ↔ 𝐵 ∈ { 𝑦 ∈ 𝐷 ∣ 𝜓 } ) )