Theorem dfpss2 3834

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 3731	. 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))
2		df-ne 2933	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	2	anbi2i 732	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))
4	1, 3	bitri 264	1 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))

Syntax hints:  ¬ wn 3   ↔ wb 196   ∧ wa 383   = wceq 1632   ≠ wne 2932   ⊆ wss 3715   ⊊ wpss 3716

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 197  df-an 385  df-ne 2933  df-pss 3731

This theorem is referenced by:  dfpss3  3835  sspss  3848  psstr  3853  npss  3859  ssnelpss  3860  pssv  4159  disj4  4169  f1imapss  6687  nnsdomo  8322  pssnn  8345  inf3lem6  8705  ssfin4  9344  fin23lem25  9358  fin23lem38  9383  isf32lem2  9388  pwfseqlem4  9696  genpcl  10042  prlem934  10067  ltaddpr  10068  chnlei  28674  cvbr2  29472  cvnbtwn2  29476  cvnbtwn3  29477  cvnbtwn4  29478  dfon2lem3  32016  dfon2lem5  32018  dfon2lem6  32019  dfon2lem7  32020  dfon2lem8  32021  dfon3  32326  lcvbr2  34830  lcvnbtwn2  34835  lcvnbtwn3  34836