Metamath Proof Explorer

Theorem bj-elgab

Description: Elements of a generalized class abstraction. (Contributed by BJ, 4-Oct-2024)

Ref Expression
Hypotheses bj-elgab.nf ⊢ φ → ∀ x φ
bj-elgab.nfa ⊢ φ → Ⅎ _ x A
bj-elgab.ex ⊢ φ → A ∈ V
bj-elgab.is ⊢ φ → ∃ x A = B ∧ ψ ↔ χ
Assertion bj-elgab ⊢ φ → A ∈ B | x | ψ ↔ χ

Proof

Step Hyp Ref Expression
1 bj-elgab.nf ⊢ φ → ∀ x φ
2 bj-elgab.nfa ⊢ φ → Ⅎ _ x A
3 bj-elgab.ex ⊢ φ → A ∈ V
4 bj-elgab.is ⊢ φ → ∃ x A = B ∧ ψ ↔ χ
5 df-bj-gab ⊢ B | x | ψ = y | ∃ x B = y ∧ ψ
6 5 eleq2i ⊢ A ∈ B | x | ψ ↔ A ∈ y | ∃ x B = y ∧ ψ
7 1 adantr ⊢ φ ∧ y = A → ∀ x φ
8 nfcvd ⊢ Ⅎ _ x A → Ⅎ _ x y
9 id ⊢ Ⅎ _ x A → Ⅎ _ x A
10 8 9 nfeqd ⊢ Ⅎ _ x A → Ⅎ x y = A
11 10 nf5rd ⊢ Ⅎ _ x A → y = A → ∀ x y = A
12 2 11 syl ⊢ φ → y = A → ∀ x y = A
13 12 imp ⊢ φ ∧ y = A → ∀ x y = A
14 19.26 ⊢ ∀ x φ ∧ y = A ↔ ∀ x φ ∧ ∀ x y = A
15 7 13 14 sylanbrc ⊢ φ ∧ y = A → ∀ x φ ∧ y = A
16 eqeq2 ⊢ y = A → B = y ↔ B = A
17 eqcom ⊢ B = A ↔ A = B
18 16 17 bitrdi ⊢ y = A → B = y ↔ A = B
19 18 anbi1d ⊢ y = A → B = y ∧ ψ ↔ A = B ∧ ψ
20 19 adantl ⊢ φ ∧ y = A → B = y ∧ ψ ↔ A = B ∧ ψ
21 15 20 exbidh ⊢ φ ∧ y = A → ∃ x B = y ∧ ψ ↔ ∃ x A = B ∧ ψ
22 21 ex ⊢ φ → y = A → ∃ x B = y ∧ ψ ↔ ∃ x A = B ∧ ψ
23 22 alrimiv ⊢ φ → ∀ y y = A → ∃ x B = y ∧ ψ ↔ ∃ x A = B ∧ ψ
24 elabgt ⊢ A ∈ V ∧ ∀ y y = A → ∃ x B = y ∧ ψ ↔ ∃ x A = B ∧ ψ → A ∈ y | ∃ x B = y ∧ ψ ↔ ∃ x A = B ∧ ψ
25 3 23 24 syl2anc ⊢ φ → A ∈ y | ∃ x B = y ∧ ψ ↔ ∃ x A = B ∧ ψ
26 25 4 bitrd ⊢ φ → A ∈ y | ∃ x B = y ∧ ψ ↔ χ
27 6 26 bitrid ⊢ φ → A ∈ B | x | ψ ↔ χ