Theorem dfpss2 4020

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 3906	. 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))
2		df-ne 2944	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	2	anbi2i 623	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))
4	1, 3	bitri 274	1 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 396   = wceq 1539   ≠ wne 2943   ⊆ wss 3887   ⊊ wpss 3888

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 206  df-an 397  df-ne 2944  df-pss 3906

This theorem is referenced by:  dfpss3  4021  sspss  4034  psstr  4039  npss  4045  ssnelpss  4046  pssv  4380  disj4  4392  f1imapss  7139  pssnn  8951  phpeqd  8998  phpeqdOLD  9008  nnsdomo  9017  pssnnOLD  9040  inf3lem6  9391  ssfin4  10066  fin23lem25  10080  fin23lem38  10105  isf32lem2  10110  pwfseqlem4  10418  genpcl  10764  prlem934  10789  ltaddpr  10790  chnlei  29847  cvbr2  30645  cvnbtwn2  30649  cvnbtwn3  30650  cvnbtwn4  30651  dfon2lem3  33761  dfon2lem5  33763  dfon2lem6  33764  dfon2lem7  33765  dfon2lem8  33766  sltlpss  34087  dfon3  34194  lcvbr2  37036  lcvnbtwn2  37041  lcvnbtwn3  37042  rr-phpd  41821