Theorem prss 4351

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

Syntax hints:   ↔ wb 196   ∧ wa 384   ∈ wcel 1990  Vcvv 3200   ⊆ wss 3574  {cpr 4179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-in 3581  df-ss 3588  df-sn 4178  df-pr 4180

This theorem is referenced by:  tpss  4368  uniintsn  4514  pwssun  5020  xpsspw  5233  dffv2  6271  fpr2g  6475  fiint  8237  wunex2  9560  hashfun  13224  fun2dmnop0  13276  prdsle  16122  prdsless  16123  prdsleval  16137  pwsle  16152  acsfn2  16324  joinfval  17001  joindmss  17007  meetfval  17015  meetdmss  17021  clatl  17116  ipoval  17154  ipolerval  17156  eqgfval  17642  eqgval  17643  gaorb  17740  pmtrrn2  17880  efgcpbllema  18167  frgpuplem  18185  drngnidl  19229  drnglpir  19253  isnzr2hash  19264  ltbval  19471  ltbwe  19472  opsrle  19475  opsrtoslem1  19484  thlle  20041  isphtpc  22793  axlowdimlem4  25825  structgrssvtx  25913  structgrssiedg  25914  structgrssvtxlemOLD  25915  structgrssvtxOLD  25916  structgrssiedgOLD  25917  umgredg  26033  wlk1walk  26535  wlkonl1iedg  26561  wlkdlem2  26580  3wlkdlem6  27025  frcond2  27131  frcond3  27133  nfrgr2v  27136  frgr3vlem1  27137  frgr3vlem2  27138  2pthfrgrrn  27146  frgrncvvdeqlem2  27164  shincli  28221  chincli  28319  coinfliprv  30544  altxpsspw  32084  fourierdlem103  40426  fourierdlem104  40427  nnsum3primes4  41676