Theorem dfpss2 4043

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 3926	. 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))
2		df-ne 2961	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	2	anbi2i 635	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))
4	1, 3	bitri 278	1 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∧ wa 401   = wceq 1570   ≠ wne 2960   ⊆ wss 3906   ⊊ wpss 3907

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-ne 2961  df-pss 3926

This theorem is used by:  dfpss3  4044  sspss  4057  psstr  4063  npss  4069  ssnelpss  4070  pssv  4369  disj4  4419  f1imapss  7269  pssnn  9160  phpeqd  9203  nnsdomo  9210  inf3lem6  9609  ssfin4  10309  fin23lem25  10323  fin23lem38  10348  isf32lem2  10353  pwfseqlem4  10662  genpcl  11008  prlem934  11033  ltaddpr  11034  ltslpss  28152  chnlei  31908  cvbr2  32706  cvnbtwn2  32710  cvnbtwn3  32711  cvnbtwn4  32712  dfon2lem3  36312  dfon2lem5  36314  dfon2lem6  36315  dfon2lem7  36316  dfon2lem8  36317  dfon3  36419  lcvbr2  39854  lcvnbtwn2  39859  lcvnbtwn3  39860  rr-phpd  44991