Theorem dfpss2 4019

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 3903	. 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))
2		df-ne 2935	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	2	anbi2i 629	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))
4	1, 3	bitri 276	1 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))

Syntax hints:  ¬ wn 3   ↔ wb 207   ∧ wa 396   = wceq 1547   ≠ wne 2934   ⊆ wss 3883   ⊊ wpss 3884

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 208  df-an 397  df-ne 2935  df-pss 3903

This theorem is referenced by:  dfpss3  4020  sspss  4033  psstr  4038  npss  4044  ssnelpss  4045  pssv  4377  disj4  4387  f1imapss  7210  pssnn  9093  phpeqd  9136  nnsdomo  9143  inf3lem6  9545  ssfin4  10223  fin23lem25  10237  fin23lem38  10262  isf32lem2  10267  pwfseqlem4  10576  genpcl  10922  prlem934  10947  ltaddpr  10948  ltslpss  27918  chnlei  31574  cvbr2  32372  cvnbtwn2  32376  cvnbtwn3  32377  cvnbtwn4  32378  dfon2lem3  36011  dfon2lem5  36013  dfon2lem6  36014  dfon2lem7  36015  dfon2lem8  36016  dfon3  36118  lcvbr2  39514  lcvnbtwn2  39519  lcvnbtwn3  39520  rr-phpd  44653