Theorem dfpss2 4014

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 4013	. 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))
2		df-ne 2956	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	2	anbi2i 635	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))
4	1, 3	bitri 278	1 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∧ wa 401   = wceq 1569   ≠ wne 2955   ⊆ wss 3896   ⊊ wpss 4012

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-ne 2956  df-pss 4013

This theorem is used by:  dfpss3  4015  sspss  4028  psstr  4034  npss  4040  ssnelpss  4041  pssv  4361  disj4  4411  f1imapss  7274  pssnn  9191  phpeqd  9234  nnsdomo  9241  inf3lem6  9641  ssfin4  10395  fin23lem25  10409  fin23lem38  10434  isf32lem2  10439  pwfseqlem4  10754  genpcl  11100  prlem934  11125  ltaddpr  11126  ltslpss  28303  chnlei  32096  cvbr2  32894  cvnbtwn2  32898  cvnbtwn3  32899  cvnbtwn4  32900  dfon2lem3  36643  dfon2lem5  36645  dfon2lem6  36646  dfon2lem7  36647  dfon2lem8  36648  dfon3  36750  lcvbr2  40188  lcvnbtwn2  40193  lcvnbtwn3  40194  rr-phpd  45316