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

Metamath Proof Explorer

Theorem elrab2w

Description: Membership in a restricted class abstraction. This is to elrab2 what elab2gw is to elab2g . (Contributed by SN, 2-Sep-2024)

Ref Expression
Hypotheses elrab2w.1 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
elrab2w.2 ⊢ ( 𝑦 = 𝐴 → ( 𝜓 ↔ 𝜒 ) )
elrab2w.3 ⊢ 𝐶 = { 𝑥 ∈ 𝐵 ∣ 𝜑 }
Assertion elrab2w ( 𝐴 ∈ 𝐶 ↔ ( 𝐴 ∈ 𝐵 ∧ 𝜒 ) )

Proof

Step Hyp Ref Expression
1 elrab2w.1 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2 elrab2w.2 ⊢ ( 𝑦 = 𝐴 → ( 𝜓 ↔ 𝜒 ) )
3 elrab2w.3 ⊢ 𝐶 = { 𝑥 ∈ 𝐵 ∣ 𝜑 }
4 elex ⊢ ( 𝐴 ∈ 𝐶 → 𝐴 ∈ V )
5 elex ⊢ ( 𝐴 ∈ 𝐵 → 𝐴 ∈ V )
6 5 adantr ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝜒 ) → 𝐴 ∈ V )
7 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵 ) )
8 7 1 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) ) )
9 eleq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
10 9 2 anbi12d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) ↔ ( 𝐴 ∈ 𝐵 ∧ 𝜒 ) ) )
11 df-rab ⊢ { 𝑥 ∈ 𝐵 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) }
12 3 11 eqtri ⊢ 𝐶 = { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) }
13 8 10 12 elab2gw ⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ 𝐶 ↔ ( 𝐴 ∈ 𝐵 ∧ 𝜒 ) ) )
14 4 6 13 pm5.21nii ⊢ ( 𝐴 ∈ 𝐶 ↔ ( 𝐴 ∈ 𝐵 ∧ 𝜒 ) )