Theorem dfpss2 3653

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 3555	. 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))
2		df-ne 2781	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	2	anbi2i 725	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))
4	1, 3	bitri 262	1 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))

Syntax hints:  ¬ wn 3   ↔ wb 194   ∧ wa 382   = wceq 1474   ≠ wne 2779   ⊆ wss 3539   ⊊ wpss 3540

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 195  df-an 384  df-ne 2781  df-pss 3555

This theorem is referenced by:  dfpss3  3654  sspss  3667  psstr  3672  npss  3678  ssnelpss  3679  pssv  3967  disj4  3976  f1imapss  6401  nnsdomo  8017  pssnn  8040  inf3lem6  8390  ssfin4  8992  fin23lem25  9006  fin23lem38  9031  isf32lem2  9036  pwfseqlem4  9340  genpcl  9686  prlem934  9711  ltaddpr  9712  isprm2lem  15180  chnlei  27521  cvbr2  28319  cvnbtwn2  28323  cvnbtwn3  28324  cvnbtwn4  28325  dfon2lem3  30727  dfon2lem5  30729  dfon2lem6  30730  dfon2lem7  30731  dfon2lem8  30732  dfon3  30962  lcvbr2  33110  lcvnbtwn2  33115  lcvnbtwn3  33116