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 ⊢ x = y → φ ↔ ψ
elrab2w.2 ⊢ y = A → ψ ↔ χ
elrab2w.3 ⊢ C = x ∈ B | φ
Assertion elrab2w ⊢ A ∈ C ↔ A ∈ B ∧ χ

Proof

Step Hyp Ref Expression
1 elrab2w.1 ⊢ x = y → φ ↔ ψ
2 elrab2w.2 ⊢ y = A → ψ ↔ χ
3 elrab2w.3 ⊢ C = x ∈ B | φ
4 elex ⊢ A ∈ C → A ∈ V
5 elex ⊢ A ∈ B → A ∈ V
6 5 adantr ⊢ A ∈ B ∧ χ → A ∈ V
7 eleq1w ⊢ x = y → x ∈ B ↔ y ∈ B
8 7 1 anbi12d ⊢ x = y → x ∈ B ∧ φ ↔ y ∈ B ∧ ψ
9 eleq1 ⊢ y = A → y ∈ B ↔ A ∈ B
10 9 2 anbi12d ⊢ y = A → y ∈ B ∧ ψ ↔ A ∈ B ∧ χ
11 df-rab ⊢ x ∈ B | φ = x | x ∈ B ∧ φ
12 3 11 eqtri ⊢ C = x | x ∈ B ∧ φ
13 8 10 12 elab2gw ⊢ A ∈ V → A ∈ C ↔ A ∈ B ∧ χ
14 4 6 13 pm5.21nii ⊢ A ∈ C ↔ A ∈ B ∧ χ