Theorem dfpss2 4098

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   = wceq 1537   ≠ wne 2938   ⊆ wss 3963   ⊊ wpss 3964

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 2939  df-pss 3983

This theorem is referenced by:  dfpss3  4099  sspss  4112  psstr  4117  npss  4123  ssnelpss  4124  pssv  4455  disj4  4465  f1imapss  7286  pssnn  9207  phpeqd  9250  phpeqdOLD  9260  nnsdomo  9268  inf3lem6  9671  ssfin4  10348  fin23lem25  10362  fin23lem38  10387  isf32lem2  10392  pwfseqlem4  10700  genpcl  11046  prlem934  11071  ltaddpr  11072  sltlpss  27960  chnlei  31514  cvbr2  32312  cvnbtwn2  32316  cvnbtwn3  32317  cvnbtwn4  32318  dfon2lem3  35767  dfon2lem5  35769  dfon2lem6  35770  dfon2lem7  35771  dfon2lem8  35772  dfon3  35874  lcvbr2  39004  lcvnbtwn2  39009  lcvnbtwn3  39010  rr-phpd  44199