Theorem dfpss2 4013

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

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 399   = wceq 1538   ≠ wne 2987   ⊆ wss 3881   ⊊ wpss 3882

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 210  df-an 400  df-ne 2988  df-pss 3900

This theorem is referenced by:  dfpss3  4014  sspss  4027  psstr  4032  npss  4038  ssnelpss  4039  pssv  4354  disj4  4366  f1imapss  7002  phpeqd  8690  nnsdomo  8698  pssnn  8720  inf3lem6  9080  ssfin4  9721  fin23lem25  9735  fin23lem38  9760  isf32lem2  9765  pwfseqlem4  10073  genpcl  10419  prlem934  10444  ltaddpr  10445  chnlei  29268  cvbr2  30066  cvnbtwn2  30070  cvnbtwn3  30071  cvnbtwn4  30072  dfon2lem3  33143  dfon2lem5  33145  dfon2lem6  33146  dfon2lem7  33147  dfon2lem8  33148  dfon3  33466  lcvbr2  36318  lcvnbtwn2  36323  lcvnbtwn3  36324  rr-phpd  40916