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 2957	. . 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 2956   ⊆ 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 2957  df-pss 3919

This theorem is used by:  dfpss3  4037  sspss  4050  psstr  4056  npss  4062  ssnelpss  4063  pssv  4362  disj4  4412  f1imapss  7268  pssnn  9177  phpeqd  9220  nnsdomo  9227  inf3lem6  9627  ssfin4  10381  fin23lem25  10395  fin23lem38  10420  isf32lem2  10425  pwfseqlem4  10740  genpcl  11086  prlem934  11111  ltaddpr  11112  ltslpss  28287  chnlei  32080  cvbr2  32878  cvnbtwn2  32882  cvnbtwn3  32883  cvnbtwn4  32884  dfon2lem3  36527  dfon2lem5  36529  dfon2lem6  36530  dfon2lem7  36531  dfon2lem8  36532  dfon3  36634  lcvbr2  40059  lcvnbtwn2  40064  lcvnbtwn3  40065  rr-phpd  45192