Theorem dfpss2 3692

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 3590	. 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))
2		df-ne 2795	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	2	anbi2i 730	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))
4	1, 3	bitri 264	1 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))

Syntax hints:  ¬ wn 3   ↔ wb 196   ∧ wa 384   = wceq 1483   ≠ wne 2794   ⊆ wss 3574   ⊊ wpss 3575

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 197  df-an 386  df-ne 2795  df-pss 3590

This theorem is referenced by:  dfpss3  3693  sspss  3706  psstr  3711  npss  3717  ssnelpss  3718  pssv  4016  disj4  4025  f1imapss  6523  nnsdomo  8155  pssnn  8178  inf3lem6  8530  ssfin4  9132  fin23lem25  9146  fin23lem38  9171  isf32lem2  9176  pwfseqlem4  9484  genpcl  9830  prlem934  9855  ltaddpr  9856  chnlei  28344  cvbr2  29142  cvnbtwn2  29146  cvnbtwn3  29147  cvnbtwn4  29148  dfon2lem3  31690  dfon2lem5  31692  dfon2lem6  31693  dfon2lem7  31694  dfon2lem8  31695  dfon3  31999  lcvbr2  34309  lcvnbtwn2  34314  lcvnbtwn3  34315