Theorem prss 4832

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

Syntax hints:   ↔ wb 205   ∧ wa 394   ∈ wcel 2100  Vcvv 3472   ⊆ wss 3959  {cpr 4638

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-ext 2700

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-ex 1775  df-sb 2062  df-clab 2707  df-cleq 2721  df-clel 2806  df-v 3474  df-un 3964  df-ss 3976  df-sn 4637  df-pr 4639

This theorem is referenced by:  tpss  4849  uniintsn  5000  pwssun  5581  xpsspw  5819  dffv2  7002  fiint  9375  fiintOLD  9376  wunex2  10788  hashfun  14466  fun2dmnop0  14534  prdsle  17498  prdsless  17499  prdsleval  17513  pwsle  17528  acsfn2  17697  joinfval  18419  joindmss  18425  meetfval  18433  meetdmss  18439  clatl  18554  ipoval  18576  ipolerval  18578  eqgfval  19192  eqgval  19193  eqg0subg  19212  gaorb  19323  pmtrrn2  19480  efgcpbllema  19774  frgpuplem  19792  isnzr2hash  20523  thlle  21716  thlleOLD  21717  ltbval  22072  ltbwe  22073  opsrle  22076  opsrtoslem1  22090  isphtpc  25034  axlowdimlem4  28902  structgrssvtx  28983  structgrssiedg  28984  umgredg  29097  wlk1walk  29599  wlkonl1iedg  29625  wlkdlem2  29643  3wlkdlem6  30121  frcond2  30223  frcond3  30225  nfrgr2v  30228  frgr3vlem1  30229  frgr3vlem2  30230  2pthfrgrrn  30238  frgrncvvdeqlem2  30256  shincli  31318  chincli  31416  lsmsnorb  33311  quslsm  33325  coinfliprv  34374  altxpsspw  35868  mnurndlem1  44046  fourierdlem103  45920  fourierdlem104  45921  nnsum3primes4  47450