Theorem prss 4781

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 4780	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶))
4	1, 2, 3	mp2an 704	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶)

Syntax hints:   ↔ wb 209   ∧ wa 400   ∈ wcel 2145  Vcvv 3457   ⊆ wss 3907  {cpr 4587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912  df-ss 3924  df-sn 4586  df-pr 4588

This theorem is referenced by:  tpss  4797  uniintsn  4945  pwssun  5543  xpsspw  5786  dffv2  6966  fiint  9274  wunex2  10711  hashfun  14462  fun2dmnop0  14529  prdsle  17503  prdsless  17504  prdsleval  17518  pwsle  17534  acsfn2  17707  joinfval  18415  joindmss  18421  meetfval  18429  meetdmss  18435  clatl  18552  ipoval  18574  ipolerval  18576  eqgfval  19232  eqgval  19233  eqg0subg  19255  gaorb  19365  pmtrrn2  19518  efgcpbllema  19812  frgpuplem  19830  isnzr2hash  20591  thlle  21804  ltbval  22151  ltbwe  22152  opsrle  22155  opsrtoslem1  22163  isphtpc  25110  axlowdimlem4  29200  structgrssvtx  29279  structgrssiedg  29280  umgredg  29393  wlk1walk  29893  wlkonl1iedg  29918  wlkdlem2  29936  3wlkdlem6  30421  frcond2  30523  frcond3  30525  nfrgr2v  30528  frgr3vlem1  30529  frgr3vlem2  30530  2pthfrgrrn  30538  frgrncvvdeqlem2  30556  shincli  31619  chincli  31717  lsmsnorb  33615  quslsm  33625  coinfliprv  34785  altxpsspw  36335  mnurndlem1  44850  fourierdlem103  46782  fourierdlem104  46783  nnsum3primes4  48409  isubgr3stgrlem6  48592  grlimprclnbgrvtx  48620  grlimgrtrilem2  48623  gpgprismgr4cycllem8  48723  pgnbgreunbgr  48746