Theorem dfpss3 4041

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 4040	. 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))
2		eqss 3949	. . . . 5 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
3	2	baib 535	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 = 𝐵 ↔ 𝐵 ⊆ 𝐴))
4	3	notbid 318	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (¬ 𝐴 = 𝐵 ↔ ¬ 𝐵 ⊆ 𝐴))
5	4	pm5.32i 574	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴))
6	1, 5	bitri 275	1 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴))

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   = wceq 1541   ⊆ wss 3901   ⊊ wpss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ne 2933  df-ss 3918  df-pss 3921

This theorem is referenced by:  pssirr  4055  pssn2lp  4056  ssnpss  4058  nsspssun  4220  pssdifcom1  4442  pssdifcom2  4443  php3  9133  fincssdom  10233  reclem2pr  10959  ressval3d  17173  islbs3  21110  ltslpss  27904  chpsscon3  31578  chpssati  32438  fundmpss  35961  lpssat  39283  lssat  39286  dihglblem6  41610  pssnssi  45355  mbfpsssmf  47037