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 705	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶)

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2147  Vcvv 3454   ⊆ wss 3900  {cpr 4590

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154  df-sn 4589  df-pr 4591

This theorem is used by:  tpss  4797  uniintsn  4950  pwssun  5550  xpsspw  5796  dffv2  7011  fiint  9356  wunex2  10862  hashfun  14623  fun2dmnop0  14690  prdsle  17683  prdsless  17684  prdsleval  17698  pwsle  17714  acsfn2  17887  joinfval  18595  joindmss  18601  meetfval  18609  meetdmss  18615  clatl  18732  ipoval  18754  ipolerval  18756  eqgfval  19438  eqgval  19439  eqg0subg  19461  gaorb  19572  pmtrrn2  19725  efgcpbllema  20019  frgpuplem  20037  isnzr2hash  20821  thlle  22058  ltbval  22407  ltbwe  22408  opsrle  22411  opsrtoslem1  22419  isphtpc  25370  axlowdimlem4  29580  structgrssvtx  29659  structgrssiedg  29660  umgredg  29773  wlk1walk  30276  wlkonl1iedg  30301  wlkdlem2  30319  3wlkdlem6  30823  frcond2  30925  frcond3  30927  nfrgr2v  30930  frgr3vlem1  30931  frgr3vlem2  30932  2pthfrgrrn  30940  frgrncvvdeqlem2  30958  shincli  32021  chincli  32119  lsmsnorb  34050  quslsm  34060  coinfliprv  35226  altxpsspw  36957  mnurndlem1  45526  fourierdlem103  47492  fourierdlem104  47493  nnsum3primes4  49159  isubgr3stgrlem6  49342  grlimprclnbgrvtx  49370  grlimgrtrilem2  49373  gpgprismgr4cycllem8  49473  pgnbgreunbgr  49496