Theorem prss 4750

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

Syntax hints:   ↔ wb 205   ∧ wa 395   ∈ wcel 2108  Vcvv 3422   ⊆ wss 3883  {cpr 4560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-in 3890  df-ss 3900  df-sn 4559  df-pr 4561

This theorem is referenced by:  tpss  4765  uniintsn  4915  pwssun  5476  xpsspw  5708  dffv2  6845  fiint  9021  wunex2  10425  hashfun  14080  fun2dmnop0  14136  prdsle  17090  prdsless  17091  prdsleval  17105  pwsle  17120  acsfn2  17289  joinfval  18006  joindmss  18012  meetfval  18020  meetdmss  18026  clatl  18141  ipoval  18163  ipolerval  18165  eqgfval  18719  eqgval  18720  gaorb  18828  pmtrrn2  18983  efgcpbllema  19275  frgpuplem  19293  isnzr2hash  20448  thlle  20814  ltbval  21154  ltbwe  21155  opsrle  21158  opsrtoslem1  21172  isphtpc  24063  axlowdimlem4  27216  structgrssvtx  27297  structgrssiedg  27298  umgredg  27411  wlk1walk  27908  wlkonl1iedg  27935  wlkdlem2  27953  3wlkdlem6  28430  frcond2  28532  frcond3  28534  nfrgr2v  28537  frgr3vlem1  28538  frgr3vlem2  28539  2pthfrgrrn  28547  frgrncvvdeqlem2  28565  shincli  29625  chincli  29723  lsmsnorb  31481  quslsm  31495  coinfliprv  32349  altxpsspw  34206  mnurndlem1  41788  fourierdlem103  43640  fourierdlem104  43641  nnsum3primes4  45128