Theorem prss 4819

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2107  Vcvv 3479   ⊆ wss 3950  {cpr 4627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-un 3955  df-ss 3967  df-sn 4626  df-pr 4628

This theorem is referenced by:  tpss  4836  uniintsn  4984  pwssun  5574  xpsspw  5818  dffv2  7003  fiint  9367  fiintOLD  9368  wunex2  10779  hashfun  14477  fun2dmnop0  14544  prdsle  17508  prdsless  17509  prdsleval  17523  pwsle  17538  acsfn2  17707  joinfval  18419  joindmss  18425  meetfval  18433  meetdmss  18439  clatl  18554  ipoval  18576  ipolerval  18578  eqgfval  19195  eqgval  19196  eqg0subg  19215  gaorb  19326  pmtrrn2  19479  efgcpbllema  19773  frgpuplem  19791  isnzr2hash  20520  thlle  21717  thlleOLD  21718  ltbval  22062  ltbwe  22063  opsrle  22066  opsrtoslem1  22080  isphtpc  25027  axlowdimlem4  28961  structgrssvtx  29042  structgrssiedg  29043  umgredg  29156  wlk1walk  29658  wlkonl1iedg  29684  wlkdlem2  29702  3wlkdlem6  30185  frcond2  30287  frcond3  30289  nfrgr2v  30292  frgr3vlem1  30293  frgr3vlem2  30294  2pthfrgrrn  30302  frgrncvvdeqlem2  30320  shincli  31382  chincli  31480  lsmsnorb  33420  quslsm  33434  coinfliprv  34486  altxpsspw  35979  mnurndlem1  44305  fourierdlem103  46229  fourierdlem104  46230  nnsum3primes4  47780  isubgr3stgrlem6  47943  grlimgrtrilem2  47967