Metamath Proof Explorer

Theorem abnex

Description: Sufficient condition for a class abstraction to be a proper class. Lemma for snnex and pwnex . See the comment of abnexg . (Contributed by BJ, 2-May-2021)

Ref Expression
Assertion abnex ⊢ ∀ x F ∈ V ∧ x ∈ F → ¬ y | ∃ x y = F ∈ V

Proof

Step Hyp Ref Expression
1 vprc ⊢ ¬ V ∈ V
2 alral ⊢ ∀ x F ∈ V ∧ x ∈ F → ∀ x ∈ V F ∈ V ∧ x ∈ F
3 rexv ⊢ ∃ x ∈ V y = F ↔ ∃ x y = F
4 3 bicomi ⊢ ∃ x y = F ↔ ∃ x ∈ V y = F
5 4 abbii ⊢ y | ∃ x y = F = y | ∃ x ∈ V y = F
6 5 eleq1i ⊢ y | ∃ x y = F ∈ V ↔ y | ∃ x ∈ V y = F ∈ V
7 6 biimpi ⊢ y | ∃ x y = F ∈ V → y | ∃ x ∈ V y = F ∈ V
8 abnexg ⊢ ∀ x ∈ V F ∈ V ∧ x ∈ F → y | ∃ x ∈ V y = F ∈ V → V ∈ V
9 2 7 8 syl2im ⊢ ∀ x F ∈ V ∧ x ∈ F → y | ∃ x y = F ∈ V → V ∈ V
10 1 9 mtoi ⊢ ∀ x F ∈ V ∧ x ∈ F → ¬ y | ∃ x y = F ∈ V