Theorem dfpss2 4047

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   = wceq 1540   ≠ wne 2925   ⊆ wss 3911   ⊊ wpss 3912

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 2926  df-pss 3931

This theorem is referenced by:  dfpss3  4048  sspss  4061  psstr  4066  npss  4072  ssnelpss  4073  pssv  4408  disj4  4418  f1imapss  7223  pssnn  9109  phpeqd  9153  nnsdomo  9159  inf3lem6  9562  ssfin4  10239  fin23lem25  10253  fin23lem38  10278  isf32lem2  10283  pwfseqlem4  10591  genpcl  10937  prlem934  10962  ltaddpr  10963  sltlpss  27857  chnlei  31464  cvbr2  32262  cvnbtwn2  32266  cvnbtwn3  32267  cvnbtwn4  32268  dfon2lem3  35766  dfon2lem5  35768  dfon2lem6  35769  dfon2lem7  35770  dfon2lem8  35771  dfon3  35873  lcvbr2  39008  lcvnbtwn2  39013  lcvnbtwn3  39014  rr-phpd  44191