Theorem dfpss2 4063

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   = wceq 1540   ≠ wne 2932   ⊆ wss 3926   ⊊ wpss 3927

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 3946

This theorem is referenced by:  dfpss3  4064  sspss  4077  psstr  4082  npss  4088  ssnelpss  4089  pssv  4424  disj4  4434  f1imapss  7258  pssnn  9180  phpeqd  9224  phpeqdOLD  9232  nnsdomo  9240  inf3lem6  9645  ssfin4  10322  fin23lem25  10336  fin23lem38  10361  isf32lem2  10366  pwfseqlem4  10674  genpcl  11020  prlem934  11045  ltaddpr  11046  sltlpss  27862  chnlei  31412  cvbr2  32210  cvnbtwn2  32214  cvnbtwn3  32215  cvnbtwn4  32216  dfon2lem3  35749  dfon2lem5  35751  dfon2lem6  35752  dfon2lem7  35753  dfon2lem8  35754  dfon3  35856  lcvbr2  38986  lcvnbtwn2  38991  lcvnbtwn3  38992  rr-phpd  44180