Theorem dfpss2 4042

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 3923	. 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 3903   ⊊ wpss 3904

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 3923

This theorem is referenced by:  dfpss3  4043  sspss  4056  psstr  4061  npss  4067  ssnelpss  4068  pssv  4403  disj4  4413  f1imapss  7222  pssnn  9105  phpeqd  9148  nnsdomo  9155  inf3lem6  9554  ssfin4  10232  fin23lem25  10246  fin23lem38  10271  isf32lem2  10276  pwfseqlem4  10585  genpcl  10931  prlem934  10956  ltaddpr  10957  ltslpss  27916  chnlei  31573  cvbr2  32371  cvnbtwn2  32375  cvnbtwn3  32376  cvnbtwn4  32377  dfon2lem3  35999  dfon2lem5  36001  dfon2lem6  36002  dfon2lem7  36003  dfon2lem8  36004  dfon3  36106  lcvbr2  39398  lcvnbtwn2  39403  lcvnbtwn3  39404  rr-phpd  44565