Theorem dfpss2 3914

Description: Alternate definition of proper subclass. (Contributed by NM, 7-Feb-1996.)

Assertion

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

Proof of Theorem dfpss2

Step	Hyp	Ref	Expression
1		df-pss 3808	. 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))
2		df-ne 2970	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	2	anbi2i 616	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))
4	1, 3	bitri 267	1 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))

Syntax hints:  ¬ wn 3   ↔ wb 198   ∧ wa 386   = wceq 1601   ≠ wne 2969   ⊆ wss 3792   ⊊ wpss 3793

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 199  df-an 387  df-ne 2970  df-pss 3808

This theorem is referenced by:  dfpss3  3915  sspss  3928  psstr  3933  npss  3939  ssnelpss  3940  pssv  4241  disj4  4251  f1imapss  6797  nnsdomo  8445  pssnn  8468  inf3lem6  8829  ssfin4  9469  fin23lem25  9483  fin23lem38  9508  isf32lem2  9513  pwfseqlem4  9821  genpcl  10167  prlem934  10192  ltaddpr  10193  chnlei  28933  cvbr2  29731  cvnbtwn2  29735  cvnbtwn3  29736  cvnbtwn4  29737  dfon2lem3  32286  dfon2lem5  32288  dfon2lem6  32289  dfon2lem7  32290  dfon2lem8  32291  dfon3  32596  lcvbr2  35185  lcvnbtwn2  35190  lcvnbtwn3  35191