Theorem dfpss2 4035

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   = wceq 1541   ≠ wne 2928   ⊆ wss 3897   ⊊ wpss 3898

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 2929  df-pss 3917

This theorem is referenced by:  dfpss3  4036  sspss  4049  psstr  4054  npss  4060  ssnelpss  4061  pssv  4396  disj4  4406  f1imapss  7200  pssnn  9078  phpeqd  9121  nnsdomo  9127  inf3lem6  9523  ssfin4  10201  fin23lem25  10215  fin23lem38  10240  isf32lem2  10245  pwfseqlem4  10553  genpcl  10899  prlem934  10924  ltaddpr  10925  sltlpss  27853  chnlei  31465  cvbr2  32263  cvnbtwn2  32267  cvnbtwn3  32268  cvnbtwn4  32269  dfon2lem3  35827  dfon2lem5  35829  dfon2lem6  35830  dfon2lem7  35831  dfon2lem8  35832  dfon3  35934  lcvbr2  39069  lcvnbtwn2  39074  lcvnbtwn3  39075  rr-phpd  44250