Theorem dfpss3 4043

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 4042	. 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))
2		eqss 3952	. . . . 5 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
3	2	baib 543	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 = 𝐵 ↔ 𝐵 ⊆ 𝐴))
4	3	notbid 320	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (¬ 𝐴 = 𝐵 ↔ ¬ 𝐵 ⊆ 𝐴))
5	4	pm5.32i 582	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴))
6	1, 5	bitri 277	1 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴))

Syntax hints:  ¬ wn 3   ↔ wb 208   ∧ wa 399   = wceq 1561   ⊆ wss 3905   ⊊ wpss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1801  df-cleq 2755  df-ne 2959  df-ss 3922  df-pss 3925

This theorem is referenced by:  pssirrOLD  4058  pssn2lp  4059  ssnpss  4061  nsspssun  4221  pssdifcom1  4444  pssdifcom2  4445  php3  9178  fincssdom  10281  reclem2pr  11007  ressval3d  17283  islbs3  21226  ltslpss  28002  chpsscon3  31707  chpssati  32567  fundmpss  36118  lpssat  39638  lssat  39641  dihglblem6  41965  pssnssi  45680  mbfpsssmf  47358