Metamath Proof Explorer


Theorem nssrex

Description: Negation of subclass relationship. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Assertion nssrex ( ¬ 𝐴𝐵 ↔ ∃ 𝑥𝐴 ¬ 𝑥𝐵 )

Proof

Step Hyp Ref Expression
1 nss ( ¬ 𝐴𝐵 ↔ ∃ 𝑥 ( 𝑥𝐴 ∧ ¬ 𝑥𝐵 ) )
2 df-rex ( ∃ 𝑥𝐴 ¬ 𝑥𝐵 ↔ ∃ 𝑥 ( 𝑥𝐴 ∧ ¬ 𝑥𝐵 ) )
3 1 2 bitr4i ( ¬ 𝐴𝐵 ↔ ∃ 𝑥𝐴 ¬ 𝑥𝐵 )