Theorem dfpss2 3654

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 3556	. 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))
2		df-ne 2782	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	2	anbi2i 726	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))
4	1, 3	bitri 263	1 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))

Syntax hints:  ¬ wn 3   ↔ wb 195   ∧ wa 383   = wceq 1475   ≠ wne 2780   ⊆ wss 3540   ⊊ wpss 3541

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 196  df-an 385  df-ne 2782  df-pss 3556

This theorem is referenced by:  dfpss3  3655  sspss  3668  psstr  3673  npss  3679  ssnelpss  3680  pssv  3968  disj4  3977  f1imapss  6424  nnsdomo  8040  pssnn  8063  inf3lem6  8413  ssfin4  9015  fin23lem25  9029  fin23lem38  9054  isf32lem2  9059  pwfseqlem4  9363  genpcl  9709  prlem934  9734  ltaddpr  9735  isprm2lem  15232  chnlei  27728  cvbr2  28526  cvnbtwn2  28530  cvnbtwn3  28531  cvnbtwn4  28532  dfon2lem3  30934  dfon2lem5  30936  dfon2lem6  30937  dfon2lem7  30938  dfon2lem8  30939  dfon3  31169  lcvbr2  33327  lcvnbtwn2  33332  lcvnbtwn3  33333