Theorem prss 4763

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2114  Vcvv 3429   ⊆ wss 3889  {cpr 4569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906  df-sn 4568  df-pr 4570

This theorem is referenced by:  tpss  4780  uniintsn  4927  pwssun  5523  xpsspw  5765  dffv2  6935  fiint  9237  wunex2  10661  hashfun  14399  fun2dmnop0  14466  prdsle  17425  prdsless  17426  prdsleval  17440  pwsle  17456  acsfn2  17629  joinfval  18337  joindmss  18343  meetfval  18351  meetdmss  18357  clatl  18474  ipoval  18496  ipolerval  18498  eqgfval  19151  eqgval  19152  eqg0subg  19171  gaorb  19282  pmtrrn2  19435  efgcpbllema  19729  frgpuplem  19747  isnzr2hash  20496  thlle  21677  ltbval  22021  ltbwe  22022  opsrle  22025  opsrtoslem1  22033  isphtpc  24961  axlowdimlem4  29014  structgrssvtx  29093  structgrssiedg  29094  umgredg  29207  wlk1walk  29707  wlkonl1iedg  29732  wlkdlem2  29750  3wlkdlem6  30235  frcond2  30337  frcond3  30339  nfrgr2v  30342  frgr3vlem1  30343  frgr3vlem2  30344  2pthfrgrrn  30352  frgrncvvdeqlem2  30370  shincli  31433  chincli  31531  lsmsnorb  33451  quslsm  33465  coinfliprv  34627  altxpsspw  36159  mnurndlem1  44708  fourierdlem103  46637  fourierdlem104  46638  nnsum3primes4  48264  isubgr3stgrlem6  48447  grlimprclnbgrvtx  48475  grlimgrtrilem2  48478  gpgprismgr4cycllem8  48578  pgnbgreunbgr  48601