Theorem dfpss3 4019

Description: Alternate definition of proper subclass. (Contributed by NM, 7-Feb-1996.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

Assertion

Ref	Expression
dfpss3	⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴))

Proof of Theorem dfpss3

Step	Hyp	Ref	Expression
1		dfpss2 4018	. 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))
2		eqss 3928	. . . . 5 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
3	2	baib 545	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 = 𝐵 ↔ 𝐵 ⊆ 𝐴))
4	3	notbid 321	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (¬ 𝐴 = 𝐵 ↔ ¬ 𝐵 ⊆ 𝐴))
5	4	pm5.32i 585	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴))
6	1, 5	bitri 278	1 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴))

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∧ wa 401   = wceq 1569   ⊆ wss 3900   ⊊ wpss 4016

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755  df-ne 2960  df-ss 3901  df-pss 4017

This theorem is used by:  pssirrOLD  4034  pssn2lp  4035  ssnpss  4037  nsspssun  4216  pssdifcom1  4448  pssdifcom2  4449  php3  9238  fincssdom  10414  reclem2pr  11146  ressval3d  17439  islbs3  21448  ltslpss  28309  chpsscon3  32120  chpssati  32980  fundmpss  36662  lpssat  40213  lssat  40216  dihglblem6  42540  pssnssi  46258  mbfpsssmf  47935