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

Metamath Proof Explorer

Theorem elrabf

Description: Membership in a restricted class abstraction, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable restrictions. (Contributed by NM, 21-Sep-2003)

Ref Expression
Hypotheses elrabf.1 ⊢ Ⅎ 𝑥 𝐴
elrabf.2 ⊢ Ⅎ 𝑥 𝐵
elrabf.3 ⊢ Ⅎ 𝑥 𝜓
elrabf.4 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion elrabf ( 𝐴 ∈ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ↔ ( 𝐴 ∈ 𝐵 ∧ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 elrabf.1 ⊢ Ⅎ 𝑥 𝐴
2 elrabf.2 ⊢ Ⅎ 𝑥 𝐵
3 elrabf.3 ⊢ Ⅎ 𝑥 𝜓
4 elrabf.4 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
5 elex ⊢ ( 𝐴 ∈ { 𝑥 ∈ 𝐵 ∣ 𝜑 } → 𝐴 ∈ V )
6 elex ⊢ ( 𝐴 ∈ 𝐵 → 𝐴 ∈ V )
7 6 adantr ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝜓 ) → 𝐴 ∈ V )
8 df-rab ⊢ { 𝑥 ∈ 𝐵 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) }
9 8 eleq2i ⊢ ( 𝐴 ∈ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ↔ 𝐴 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) } )
10 1 2 nfel ⊢ Ⅎ 𝑥 𝐴 ∈ 𝐵
11 10 3 nfan ⊢ Ⅎ 𝑥 ( 𝐴 ∈ 𝐵 ∧ 𝜓 )
12 eleq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
13 12 4 anbi12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ↔ ( 𝐴 ∈ 𝐵 ∧ 𝜓 ) ) )
14 1 11 13 elabgf ⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) } ↔ ( 𝐴 ∈ 𝐵 ∧ 𝜓 ) ) )
15 9 14 bitrid ⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ↔ ( 𝐴 ∈ 𝐵 ∧ 𝜓 ) ) )
16 5 7 15 pm5.21nii ⊢ ( 𝐴 ∈ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ↔ ( 𝐴 ∈ 𝐵 ∧ 𝜓 ) )