Theorem dfpss2 4018

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 4017	. 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))
2		df-ne 2960	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	2	anbi2i 635	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))
4	1, 3	bitri 278	1 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-ne 2960  df-pss 4017

This theorem is used by:  dfpss3  4019  sspss  4032  psstr  4038  npss  4044  ssnelpss  4045  pssv  4365  disj4  4415  f1imapss  7301  pssnn  9222  phpeqd  9265  nnsdomo  9272  inf3lem6  9671  ssfin4  10427  fin23lem25  10441  fin23lem38  10466  isf32lem2  10471  pwfseqlem4  10786  genpcl  11132  prlem934  11157  ltaddpr  11158  ltslpss  28351  chnlei  32144  cvbr2  32942  cvnbtwn2  32946  cvnbtwn3  32947  cvnbtwn4  32948  dfon2lem3  36762  dfon2lem5  36764  dfon2lem6  36765  dfon2lem7  36766  dfon2lem8  36767  dfon3  36869  lcvbr2  40345  lcvnbtwn2  40350  lcvnbtwn3  40351  rr-phpd  45468