Theorem dfpss2 4036

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 3919	. 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 1570   ≠ wne 2955   ⊆ wss 3899   ⊊ wpss 3900

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 3919

This theorem is used by:  dfpss3  4037  sspss  4050  psstr  4056  npss  4062  ssnelpss  4063  pssv  4362  disj4  4412  f1imapss  7263  pssnn  9163  phpeqd  9206  nnsdomo  9213  inf3lem6  9612  ssfin4  10312  fin23lem25  10326  fin23lem38  10351  isf32lem2  10356  pwfseqlem4  10671  genpcl  11017  prlem934  11042  ltaddpr  11043  ltslpss  28173  chnlei  31966  cvbr2  32764  cvnbtwn2  32768  cvnbtwn3  32769  cvnbtwn4  32770  dfon2lem3  36362  dfon2lem5  36364  dfon2lem6  36365  dfon2lem7  36366  dfon2lem8  36367  dfon3  36469  lcvbr2  39895  lcvnbtwn2  39900  lcvnbtwn3  39901  rr-phpd  45047