Theorem dfpss2 4086

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

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 397   = wceq 1542   ≠ wne 2941   ⊆ wss 3949   ⊊ wpss 3950

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 206  df-an 398  df-ne 2942  df-pss 3968

This theorem is referenced by:  dfpss3  4087  sspss  4100  psstr  4105  npss  4111  ssnelpss  4112  pssv  4447  disj4  4459  f1imapss  7265  pssnn  9168  phpeqd  9215  phpeqdOLD  9225  nnsdomo  9234  pssnnOLD  9265  inf3lem6  9628  ssfin4  10305  fin23lem25  10319  fin23lem38  10344  isf32lem2  10349  pwfseqlem4  10657  genpcl  11003  prlem934  11028  ltaddpr  11029  sltlpss  27401  chnlei  30738  cvbr2  31536  cvnbtwn2  31540  cvnbtwn3  31541  cvnbtwn4  31542  dfon2lem3  34757  dfon2lem5  34759  dfon2lem6  34760  dfon2lem7  34761  dfon2lem8  34762  dfon3  34864  lcvbr2  37892  lcvnbtwn2  37897  lcvnbtwn3  37898  rr-phpd  42962