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

Metamath Proof Explorer

Theorem elrab3

Description: Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 5-Oct-2006)

Ref Expression
Hypothesis elrab.1 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion elrab3 ( 𝐴 ∈ 𝐵 → ( 𝐴 ∈ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ↔ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 elrab.1 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2 1 elrab ⊢ ( 𝐴 ∈ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ↔ ( 𝐴 ∈ 𝐵 ∧ 𝜓 ) )
3 2 baib ⊢ ( 𝐴 ∈ 𝐵 → ( 𝐴 ∈ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ↔ 𝜓 ) )