Theorem dfpss2 3725

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

Syntax hints:  ¬ wn 3   ↔ wb 196   ∧ wa 383   = wceq 1523   ≠ wne 2823   ⊆ wss 3607   ⊊ wpss 3608

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 385  df-ne 2824  df-pss 3623

This theorem is referenced by:  dfpss3  3726  sspss  3739  psstr  3744  npss  3750  ssnelpss  3751  pssv  4049  disj4  4058  f1imapss  6563  nnsdomo  8196  pssnn  8219  inf3lem6  8568  ssfin4  9170  fin23lem25  9184  fin23lem38  9209  isf32lem2  9214  pwfseqlem4  9522  genpcl  9868  prlem934  9893  ltaddpr  9894  chnlei  28472  cvbr2  29270  cvnbtwn2  29274  cvnbtwn3  29275  cvnbtwn4  29276  dfon2lem3  31814  dfon2lem5  31816  dfon2lem6  31817  dfon2lem7  31818  dfon2lem8  31819  dfon3  32124  lcvbr2  34627  lcvnbtwn2  34632  lcvnbtwn3  34633