Theorem dfpss2 4050

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

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 400   = wceq 1567   ≠ wne 2964   ⊆ wss 3913   ⊊ wpss 3914

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 210  df-an 401  df-ne 2965  df-pss 3933

This theorem is referenced by:  dfpss3  4051  sspss  4064  psstr  4070  npss  4076  ssnelpss  4077  pssv  4375  disj4  4425  f1imapss  7265  pssnn  9152  phpeqd  9195  nnsdomo  9202  inf3lem6  9601  ssfin4  10293  fin23lem25  10307  fin23lem38  10332  isf32lem2  10337  pwfseqlem4  10646  genpcl  10992  prlem934  11017  ltaddpr  11018  ltslpss  28066  chnlei  31777  cvbr2  32575  cvnbtwn2  32579  cvnbtwn3  32580  cvnbtwn4  32581  dfon2lem3  36173  dfon2lem5  36175  dfon2lem6  36176  dfon2lem7  36177  dfon2lem8  36178  dfon3  36280  lcvbr2  39685  lcvnbtwn2  39690  lcvnbtwn3  39691  rr-phpd  44824