Theorem dfpss2 4062

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

Syntax hints:  ¬ wn 3   ↔ wb 208   ∧ wa 398   = wceq 1537   ≠ wne 3016   ⊆ wss 3936   ⊊ wpss 3937

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 399  df-ne 3017  df-pss 3954

This theorem is referenced by:  dfpss3  4063  sspss  4076  psstr  4081  npss  4087  ssnelpss  4088  pssv  4398  disj4  4408  f1imapss  7024  phpeqd  8706  nnsdomo  8713  pssnn  8736  inf3lem6  9096  ssfin4  9732  fin23lem25  9746  fin23lem38  9771  isf32lem2  9776  pwfseqlem4  10084  genpcl  10430  prlem934  10455  ltaddpr  10456  chnlei  29262  cvbr2  30060  cvnbtwn2  30064  cvnbtwn3  30065  cvnbtwn4  30066  dfon2lem3  33030  dfon2lem5  33032  dfon2lem6  33033  dfon2lem7  33034  dfon2lem8  33035  dfon3  33353  lcvbr2  36173  lcvnbtwn2  36178  lcvnbtwn3  36179  rr-phpd  40582