This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rabxfr

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