Theorem dfpss2 4085

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

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 396   = wceq 1541   ≠ wne 2940   ⊆ wss 3948   ⊊ wpss 3949

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 2941  df-pss 3967

This theorem is referenced by:  dfpss3  4086  sspss  4099  psstr  4104  npss  4110  ssnelpss  4111  pssv  4446  disj4  4458  f1imapss  7267  pssnn  9170  phpeqd  9217  phpeqdOLD  9227  nnsdomo  9236  pssnnOLD  9267  inf3lem6  9630  ssfin4  10307  fin23lem25  10321  fin23lem38  10346  isf32lem2  10351  pwfseqlem4  10659  genpcl  11005  prlem934  11030  ltaddpr  11031  sltlpss  27626  chnlei  30993  cvbr2  31791  cvnbtwn2  31795  cvnbtwn3  31796  cvnbtwn4  31797  dfon2lem3  35049  dfon2lem5  35051  dfon2lem6  35052  dfon2lem7  35053  dfon2lem8  35054  dfon3  35156  lcvbr2  38195  lcvnbtwn2  38200  lcvnbtwn3  38201  rr-phpd  43264