Theorem dfpss2 4111

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   = wceq 1537   ≠ wne 2946   ⊆ wss 3976   ⊊ wpss 3977

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 2947  df-pss 3996

This theorem is referenced by:  dfpss3  4112  sspss  4125  psstr  4130  npss  4136  ssnelpss  4137  pssv  4472  disj4  4482  f1imapss  7303  pssnn  9234  phpeqd  9278  phpeqdOLD  9288  nnsdomo  9297  inf3lem6  9702  ssfin4  10379  fin23lem25  10393  fin23lem38  10418  isf32lem2  10423  pwfseqlem4  10731  genpcl  11077  prlem934  11102  ltaddpr  11103  sltlpss  27963  chnlei  31517  cvbr2  32315  cvnbtwn2  32319  cvnbtwn3  32320  cvnbtwn4  32321  dfon2lem3  35749  dfon2lem5  35751  dfon2lem6  35752  dfon2lem7  35753  dfon2lem8  35754  dfon3  35856  lcvbr2  38978  lcvnbtwn2  38983  lcvnbtwn3  38984  rr-phpd  44172