Theorem dfpss2 4015

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 4014	. 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))
2		df-ne 2956	. . 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 1569   ≠ wne 2955   ⊆ wss 3895   ⊊ wpss 4013

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 2956  df-pss 4014

This theorem is used by:  dfpss3  4016  sspss  4029  psstr  4035  npss  4041  ssnelpss  4042  pssv  4361  disj4  4411  f1imapss  7270  pssnn  9184  phpeqd  9227  nnsdomo  9234  inf3lem6  9634  ssfin4  10388  fin23lem25  10402  fin23lem38  10427  isf32lem2  10432  pwfseqlem4  10747  genpcl  11093  prlem934  11118  ltaddpr  11119  ltslpss  28294  chnlei  32087  cvbr2  32885  cvnbtwn2  32889  cvnbtwn3  32890  cvnbtwn4  32891  dfon2lem3  36547  dfon2lem5  36549  dfon2lem6  36550  dfon2lem7  36551  dfon2lem8  36552  dfon3  36654  lcvbr2  40080  lcvnbtwn2  40085  lcvnbtwn3  40086  rr-phpd  45207