Theorem dfpss2 4040

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   = wceq 1541   ≠ wne 2932   ⊆ wss 3901   ⊊ wpss 3902

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 207  df-an 396  df-ne 2933  df-pss 3921

This theorem is referenced by:  dfpss3  4041  sspss  4054  psstr  4059  npss  4065  ssnelpss  4066  pssv  4401  disj4  4411  f1imapss  7212  pssnn  9093  phpeqd  9136  nnsdomo  9143  inf3lem6  9542  ssfin4  10220  fin23lem25  10234  fin23lem38  10259  isf32lem2  10264  pwfseqlem4  10573  genpcl  10919  prlem934  10944  ltaddpr  10945  ltslpss  27904  chnlei  31560  cvbr2  32358  cvnbtwn2  32362  cvnbtwn3  32363  cvnbtwn4  32364  dfon2lem3  35977  dfon2lem5  35979  dfon2lem6  35980  dfon2lem7  35981  dfon2lem8  35982  dfon3  36084  lcvbr2  39282  lcvnbtwn2  39287  lcvnbtwn3  39288  rr-phpd  44450