Theorem dfpss2 4054

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   = wceq 1540   ≠ wne 2926   ⊆ wss 3917   ⊊ wpss 3918

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 2927  df-pss 3937

This theorem is referenced by:  dfpss3  4055  sspss  4068  psstr  4073  npss  4079  ssnelpss  4080  pssv  4415  disj4  4425  f1imapss  7244  pssnn  9138  phpeqd  9182  nnsdomo  9188  inf3lem6  9593  ssfin4  10270  fin23lem25  10284  fin23lem38  10309  isf32lem2  10314  pwfseqlem4  10622  genpcl  10968  prlem934  10993  ltaddpr  10994  sltlpss  27826  chnlei  31421  cvbr2  32219  cvnbtwn2  32223  cvnbtwn3  32224  cvnbtwn4  32225  dfon2lem3  35780  dfon2lem5  35782  dfon2lem6  35783  dfon2lem7  35784  dfon2lem8  35785  dfon3  35887  lcvbr2  39022  lcvnbtwn2  39027  lcvnbtwn3  39028  rr-phpd  44205