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  27795  chnlei  31387  cvbr2  32185  cvnbtwn2  32189  cvnbtwn3  32190  cvnbtwn4  32191  dfon2lem3  35746  dfon2lem5  35748  dfon2lem6  35749  dfon2lem7  35750  dfon2lem8  35751  dfon3  35853  lcvbr2  38988  lcvnbtwn2  38993  lcvnbtwn3  38994  rr-phpd  44171