Theorem prss 4824

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

Syntax hints:   ↔ wb 205   ∧ wa 397   ∈ wcel 2107  Vcvv 3475   ⊆ wss 3949  {cpr 4631

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-in 3956  df-ss 3966  df-sn 4630  df-pr 4632

This theorem is referenced by:  tpss  4839  uniintsn  4992  pwssun  5572  xpsspw  5810  dffv2  6987  fiint  9324  wunex2  10733  hashfun  14397  fun2dmnop0  14455  prdsle  17408  prdsless  17409  prdsleval  17423  pwsle  17438  acsfn2  17607  joinfval  18326  joindmss  18332  meetfval  18340  meetdmss  18346  clatl  18461  ipoval  18483  ipolerval  18485  eqgfval  19056  eqgval  19057  eqg0subg  19073  gaorb  19171  pmtrrn2  19328  efgcpbllema  19622  frgpuplem  19640  isnzr2hash  20298  thlle  21251  thlleOLD  21252  ltbval  21598  ltbwe  21599  opsrle  21602  opsrtoslem1  21616  isphtpc  24510  axlowdimlem4  28203  structgrssvtx  28284  structgrssiedg  28285  umgredg  28398  wlk1walk  28896  wlkonl1iedg  28922  wlkdlem2  28940  3wlkdlem6  29418  frcond2  29520  frcond3  29522  nfrgr2v  29525  frgr3vlem1  29526  frgr3vlem2  29527  2pthfrgrrn  29535  frgrncvvdeqlem2  29553  shincli  30615  chincli  30713  lsmsnorb  32501  quslsm  32516  coinfliprv  33481  altxpsspw  34949  mnurndlem1  43040  fourierdlem103  44925  fourierdlem104  44926  nnsum3primes4  46456