Theorem prss 4713

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

Syntax hints:   ↔ wb 209   ∧ wa 399   ∈ wcel 2111  Vcvv 3409   ⊆ wss 3860  {cpr 4527

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-un 3865  df-in 3867  df-ss 3877  df-sn 4526  df-pr 4528

This theorem is referenced by:  tpss  4728  uniintsn  4880  pwssun  5430  xpsspw  5656  dffv2  6752  fiint  8841  wunex2  10211  hashfun  13861  fun2dmnop0  13917  prdsle  16807  prdsless  16808  prdsleval  16822  pwsle  16837  acsfn2  17006  joinfval  17691  joindmss  17697  meetfval  17705  meetdmss  17711  clatl  17806  ipoval  17844  ipolerval  17846  eqgfval  18409  eqgval  18410  gaorb  18518  pmtrrn2  18669  efgcpbllema  18961  frgpuplem  18979  isnzr2hash  20119  thlle  20476  ltbval  20817  ltbwe  20818  opsrle  20821  opsrtoslem1  20829  isphtpc  23709  axlowdimlem4  26852  structgrssvtx  26930  structgrssiedg  26931  umgredg  27044  wlk1walk  27541  wlkonl1iedg  27568  wlkdlem2  27586  3wlkdlem6  28063  frcond2  28165  frcond3  28167  nfrgr2v  28170  frgr3vlem1  28171  frgr3vlem2  28172  2pthfrgrrn  28180  frgrncvvdeqlem2  28198  shincli  29258  chincli  29356  lsmsnorb  31113  quslsm  31127  coinfliprv  31981  altxpsspw  33863  mnurndlem1  41407  fourierdlem103  43262  fourierdlem104  43263  nnsum3primes4  44732