Theorem dfpss2 4038

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   = wceq 1541   ≠ wne 2930   ⊆ wss 3899   ⊊ wpss 3900

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 2931  df-pss 3919

This theorem is referenced by:  dfpss3  4039  sspss  4052  psstr  4057  npss  4063  ssnelpss  4064  pssv  4399  disj4  4409  f1imapss  7210  pssnn  9091  phpeqd  9134  nnsdomo  9141  inf3lem6  9540  ssfin4  10218  fin23lem25  10232  fin23lem38  10257  isf32lem2  10262  pwfseqlem4  10571  genpcl  10917  prlem934  10942  ltaddpr  10943  sltlpss  27880  chnlei  31509  cvbr2  32307  cvnbtwn2  32311  cvnbtwn3  32312  cvnbtwn4  32313  dfon2lem3  35926  dfon2lem5  35928  dfon2lem6  35929  dfon2lem7  35930  dfon2lem8  35931  dfon3  36033  lcvbr2  39221  lcvnbtwn2  39226  lcvnbtwn3  39227  rr-phpd  44392