Theorem dfpss2 4029

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 3910	. 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))
2		df-ne 2934	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	2	anbi2i 624	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))
4	1, 3	bitri 275	1 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ ¬ 𝐴 = 𝐵))

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   = wceq 1542   ≠ wne 2933   ⊆ wss 3890   ⊊ wpss 3891

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 207  df-an 396  df-ne 2934  df-pss 3910

This theorem is referenced by:  dfpss3  4030  sspss  4043  psstr  4048  npss  4054  ssnelpss  4055  pssv  4390  disj4  4400  f1imapss  7215  pssnn  9097  phpeqd  9140  nnsdomo  9147  inf3lem6  9548  ssfin4  10226  fin23lem25  10240  fin23lem38  10265  isf32lem2  10270  pwfseqlem4  10579  genpcl  10925  prlem934  10950  ltaddpr  10951  ltslpss  27917  chnlei  31574  cvbr2  32372  cvnbtwn2  32376  cvnbtwn3  32377  cvnbtwn4  32378  dfon2lem3  35984  dfon2lem5  35986  dfon2lem6  35987  dfon2lem7  35988  dfon2lem8  35989  dfon3  36091  lcvbr2  39485  lcvnbtwn2  39490  lcvnbtwn3  39491  rr-phpd  44657