Theorem prss 4753

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

Syntax hints:   ↔ wb 205   ∧ wa 396   ∈ wcel 2106  Vcvv 3432   ⊆ wss 3887  {cpr 4563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892  df-in 3894  df-ss 3904  df-sn 4562  df-pr 4564

This theorem is referenced by:  tpss  4768  uniintsn  4918  pwssun  5485  xpsspw  5719  dffv2  6863  fiint  9091  wunex2  10494  hashfun  14152  fun2dmnop0  14208  prdsle  17173  prdsless  17174  prdsleval  17188  pwsle  17203  acsfn2  17372  joinfval  18091  joindmss  18097  meetfval  18105  meetdmss  18111  clatl  18226  ipoval  18248  ipolerval  18250  eqgfval  18804  eqgval  18805  gaorb  18913  pmtrrn2  19068  efgcpbllema  19360  frgpuplem  19378  isnzr2hash  20535  thlle  20903  thlleOLD  20904  ltbval  21244  ltbwe  21245  opsrle  21248  opsrtoslem1  21262  isphtpc  24157  axlowdimlem4  27313  structgrssvtx  27394  structgrssiedg  27395  umgredg  27508  wlk1walk  28006  wlkonl1iedg  28033  wlkdlem2  28051  3wlkdlem6  28529  frcond2  28631  frcond3  28633  nfrgr2v  28636  frgr3vlem1  28637  frgr3vlem2  28638  2pthfrgrrn  28646  frgrncvvdeqlem2  28664  shincli  29724  chincli  29822  lsmsnorb  31579  quslsm  31593  coinfliprv  32449  altxpsspw  34279  mnurndlem1  41899  fourierdlem103  43750  fourierdlem104  43751  nnsum3primes4  45240