Theorem prss 4654

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

Syntax hints:   ↔ wb 207   ∧ wa 396   ∈ wcel 2079  Vcvv 3432   ⊆ wss 3854  {cpr 4468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-v 3434  df-un 3859  df-in 3861  df-ss 3869  df-sn 4467  df-pr 4469

This theorem is referenced by:  tpss  4669  uniintsn  4813  pwssun  5336  xpsspw  5560  dffv2  6615  fiint  8631  wunex2  9995  hashfun  13634  fun2dmnop0  13686  prdsle  16552  prdsless  16553  prdsleval  16567  pwsle  16582  acsfn2  16751  joinfval  17428  joindmss  17434  meetfval  17442  meetdmss  17448  clatl  17543  ipoval  17581  ipolerval  17583  eqgfval  18069  eqgval  18070  gaorb  18166  pmtrrn2  18307  efgcpbllema  18595  frgpuplem  18613  isnzr2hash  19714  ltbval  19927  ltbwe  19928  opsrle  19931  opsrtoslem1  19939  thlle  20511  isphtpc  23269  axlowdimlem4  26402  structgrssvtx  26480  structgrssiedg  26481  umgredg  26594  wlk1walk  27091  wlkonl1iedg  27117  wlkdlem2  27138  3wlkdlem6  27619  frcond2  27726  frcond3  27728  nfrgr2v  27731  frgr3vlem1  27732  frgr3vlem2  27733  2pthfrgrrn  27741  frgrncvvdeqlem2  27759  shincli  28818  chincli  28916  coinfliprv  31313  altxpsspw  32992  mnurndlem1  40066  fourierdlem103  41990  fourierdlem104  41991  nnsum3primes4  43389