Theorem dfpss2 4051

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   = wceq 1540   ≠ wne 2925   ⊆ wss 3914   ⊊ wpss 3915

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 2926  df-pss 3934

This theorem is referenced by:  dfpss3  4052  sspss  4065  psstr  4070  npss  4076  ssnelpss  4077  pssv  4412  disj4  4422  f1imapss  7241  pssnn  9132  phpeqd  9176  nnsdomo  9182  inf3lem6  9586  ssfin4  10263  fin23lem25  10277  fin23lem38  10302  isf32lem2  10307  pwfseqlem4  10615  genpcl  10961  prlem934  10986  ltaddpr  10987  sltlpss  27819  chnlei  31414  cvbr2  32212  cvnbtwn2  32216  cvnbtwn3  32217  cvnbtwn4  32218  dfon2lem3  35773  dfon2lem5  35775  dfon2lem6  35776  dfon2lem7  35777  dfon2lem8  35778  dfon3  35880  lcvbr2  39015  lcvnbtwn2  39020  lcvnbtwn3  39021  rr-phpd  44198