Theorem dfpss3 3654

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 3653	. 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))
2		eqss 3582	. . . . 5 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
3	2	baib 941	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 = 𝐵 ↔ 𝐵 ⊆ 𝐴))
4	3	notbid 306	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (¬ 𝐴 = 𝐵 ↔ ¬ 𝐵 ⊆ 𝐴))
5	4	pm5.32i 666	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴))
6	1, 5	bitri 262	1 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴))

Syntax hints:  ¬ wn 3   ↔ wb 194   ∧ wa 382   = wceq 1474   ⊆ wss 3539   ⊊ wpss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-ne 2781  df-in 3546  df-ss 3553  df-pss 3555

This theorem is referenced by:  pssirr  3668  pssn2lp  3669  ssnpss  3671  nsspssun  3818  npss0OLD  3966  pssdifcom1  4005  pssdifcom2  4006  php3  8008  fincssdom  9005  reclem2pr  9726  ressval3d  15712  islbs3  18924  chpsscon3  27539  chpssati  28399  fundmpss  30703  lpssat  33101  lssat  33104  dihglblem6  35430  pssnssi  38095  mbfpsssmf  39452