Theorem dfpss2 4028

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

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

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 2933  df-pss 3909

This theorem is referenced by:  dfpss3  4029  sspss  4042  psstr  4047  npss  4053  ssnelpss  4054  pssv  4389  disj4  4399  f1imapss  7221  pssnn  9103  phpeqd  9146  nnsdomo  9153  inf3lem6  9554  ssfin4  10232  fin23lem25  10246  fin23lem38  10271  isf32lem2  10276  pwfseqlem4  10585  genpcl  10931  prlem934  10956  ltaddpr  10957  ltslpss  27900  chnlei  31556  cvbr2  32354  cvnbtwn2  32358  cvnbtwn3  32359  cvnbtwn4  32360  dfon2lem3  35965  dfon2lem5  35967  dfon2lem6  35968  dfon2lem7  35969  dfon2lem8  35970  dfon3  36072  lcvbr2  39468  lcvnbtwn2  39473  lcvnbtwn3  39474  rr-phpd  44636