Theorem dfpss2 4041

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 3924	. 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))
2		df-ne 2958	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	2	anbi2i 632	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))
4	1, 3	bitri 277	1 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))

Syntax hints:  ¬ wn 3   ↔ wb 208   ∧ wa 399   = wceq 1560   ≠ wne 2957   ⊆ wss 3904   ⊊ wpss 3905

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 209  df-an 400  df-ne 2958  df-pss 3924

This theorem is referenced by:  dfpss3  4042  sspss  4055  psstr  4061  npss  4067  ssnelpss  4068  pssv  4403  disj4  4413  f1imapss  7250  pssnn  9137  phpeqd  9180  nnsdomo  9187  inf3lem6  9588  ssfin4  10267  fin23lem25  10281  fin23lem38  10306  isf32lem2  10311  pwfseqlem4  10620  genpcl  10966  prlem934  10991  ltaddpr  10992  ltslpss  27998  chnlei  31685  cvbr2  32483  cvnbtwn2  32487  cvnbtwn3  32488  cvnbtwn4  32489  dfon2lem3  36130  dfon2lem5  36132  dfon2lem6  36133  dfon2lem7  36134  dfon2lem8  36135  dfon3  36237  lcvbr2  39643  lcvnbtwn2  39648  lcvnbtwn3  39649  rr-phpd  44782