Theorem prss 4383

Description: A pair of elements of a class is a subset of the class. Theorem 7.5 of [Quine] p. 49. (Contributed by NM, 30-May-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof shortened by JJ, 23-Jul-2021.)

Hypotheses

Ref	Expression
prss.1	⊢ 𝐴 ∈ V
prss.2	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
prss	⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶)

Proof of Theorem prss

Step	Hyp	Ref	Expression
1		prss.1	. 2 ⊢ 𝐴 ∈ V
2		prss.2	. 2 ⊢ 𝐵 ∈ V
3		prssg 4382	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶))
4	1, 2, 3	mp2an 708	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶)

Syntax hints:   ↔ wb 196   ∧ wa 383   ∈ wcel 2030  Vcvv 3231   ⊆ wss 3607  {cpr 4212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-un 3612  df-in 3614  df-ss 3621  df-sn 4211  df-pr 4213

This theorem is referenced by:  tpss  4400  uniintsn  4546  pwssun  5049  xpsspw  5266  dffv2  6310  fpr2g  6516  fiint  8278  wunex2  9598  hashfun  13262  fun2dmnop0  13314  prdsle  16169  prdsless  16170  prdsleval  16184  pwsle  16199  acsfn2  16371  joinfval  17048  joindmss  17054  meetfval  17062  meetdmss  17068  clatl  17163  ipoval  17201  ipolerval  17203  eqgfval  17689  eqgval  17690  gaorb  17786  pmtrrn2  17926  efgcpbllema  18213  frgpuplem  18231  drngnidl  19277  drnglpir  19301  isnzr2hash  19312  ltbval  19519  ltbwe  19520  opsrle  19523  opsrtoslem1  19532  thlle  20089  isphtpc  22840  axlowdimlem4  25870  structgrssvtx  25958  structgrssiedg  25959  structgrssvtxlemOLD  25960  structgrssvtxOLD  25961  structgrssiedgOLD  25962  umgredg  26078  wlk1walk  26591  wlkonl1iedg  26617  wlkdlem2  26636  3wlkdlem6  27143  frcond2  27247  frcond3  27249  nfrgr2v  27252  frgr3vlem1  27253  frgr3vlem2  27254  2pthfrgrrn  27262  frgrncvvdeqlem2  27280  shincli  28349  chincli  28447  coinfliprv  30672  altxpsspw  32209  fourierdlem103  40744  fourierdlem104  40745  nnsum3primes4  42001