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  7259  pssnn  9182  phpeqd  9226  phpeqdOLD  9234  nnsdomo  9242  inf3lem6  9647  ssfin4  10324  fin23lem25  10338  fin23lem38  10363  isf32lem2  10368  pwfseqlem4  10676  genpcl  11022  prlem934  11047  ltaddpr  11048  sltlpss  27871  chnlei  31466  cvbr2  32264  cvnbtwn2  32268  cvnbtwn3  32269  cvnbtwn4  32270  dfon2lem3  35803  dfon2lem5  35805  dfon2lem6  35806  dfon2lem7  35807  dfon2lem8  35808  dfon3  35910  lcvbr2  39040  lcvnbtwn2  39045  lcvnbtwn3  39046  rr-phpd  44233