Theorem prss 4770

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2110  Vcvv 3434   ⊆ wss 3900  {cpr 4576

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3436  df-un 3905  df-ss 3917  df-sn 4575  df-pr 4577

This theorem is referenced by:  tpss  4787  uniintsn  4933  pwssun  5506  xpsspw  5747  dffv2  6912  fiint  9206  wunex2  10621  hashfun  14336  fun2dmnop0  14403  prdsle  17358  prdsless  17359  prdsleval  17373  pwsle  17388  acsfn2  17561  joinfval  18269  joindmss  18275  meetfval  18283  meetdmss  18289  clatl  18406  ipoval  18428  ipolerval  18430  eqgfval  19081  eqgval  19082  eqg0subg  19101  gaorb  19212  pmtrrn2  19365  efgcpbllema  19659  frgpuplem  19677  isnzr2hash  20427  thlle  21627  ltbval  21971  ltbwe  21972  opsrle  21975  opsrtoslem1  21983  isphtpc  24913  axlowdimlem4  28916  structgrssvtx  28995  structgrssiedg  28996  umgredg  29109  wlk1walk  29610  wlkonl1iedg  29635  wlkdlem2  29653  3wlkdlem6  30135  frcond2  30237  frcond3  30239  nfrgr2v  30242  frgr3vlem1  30243  frgr3vlem2  30244  2pthfrgrrn  30252  frgrncvvdeqlem2  30270  shincli  31332  chincli  31430  lsmsnorb  33346  quslsm  33360  coinfliprv  34486  altxpsspw  35990  mnurndlem1  44293  fourierdlem103  46226  fourierdlem104  46227  nnsum3primes4  47798  isubgr3stgrlem6  47981  grlimprclnbgrvtx  48009  grlimgrtrilem2  48012  gpgprismgr4cycllem8  48112  pgnbgreunbgr  48135