Theorem dfpss2 4016

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 3902	. 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))
2		df-ne 2943	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	2	anbi2i 622	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))
4	1, 3	bitri 274	1 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 395   = wceq 1539   ≠ wne 2942   ⊆ wss 3883   ⊊ wpss 3884

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 206  df-an 396  df-ne 2943  df-pss 3902

This theorem is referenced by:  dfpss3  4017  sspss  4030  psstr  4035  npss  4041  ssnelpss  4042  pssv  4377  disj4  4389  f1imapss  7120  phpeqd  8902  pssnn  8913  nnsdomo  8948  pssnnOLD  8969  inf3lem6  9321  ssfin4  9997  fin23lem25  10011  fin23lem38  10036  isf32lem2  10041  pwfseqlem4  10349  genpcl  10695  prlem934  10720  ltaddpr  10721  chnlei  29748  cvbr2  30546  cvnbtwn2  30550  cvnbtwn3  30551  cvnbtwn4  30552  dfon2lem3  33667  dfon2lem5  33669  dfon2lem6  33670  dfon2lem7  33671  dfon2lem8  33672  sltlpss  34014  dfon3  34121  lcvbr2  36963  lcvnbtwn2  36968  lcvnbtwn3  36969  rr-phpd  41710