Theorem prss 4775

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2144  Vcvv 3450   ⊆ wss 3895  {cpr 4586

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-un 4151  df-sn 4585  df-pr 4587

This theorem is used by:  tpss  4791  uniintsn  4944  pwssun  5542  xpsspw  5786  dffv2  6981  fiint  9322  wunex2  10827  hashfun  14586  fun2dmnop0  14653  prdsle  17639  prdsless  17640  prdsleval  17654  pwsle  17670  acsfn2  17843  joinfval  18551  joindmss  18557  meetfval  18565  meetdmss  18571  clatl  18688  ipoval  18710  ipolerval  18712  eqgfval  19394  eqgval  19395  eqg0subg  19417  gaorb  19527  pmtrrn2  19680  efgcpbllema  19974  frgpuplem  19992  isnzr2hash  20776  thlle  22009  ltbval  22358  ltbwe  22359  opsrle  22362  opsrtoslem1  22370  isphtpc  25321  axlowdimlem4  29529  structgrssvtx  29608  structgrssiedg  29609  umgredg  29722  wlk1walk  30225  wlkonl1iedg  30250  wlkdlem2  30268  3wlkdlem6  30772  frcond2  30874  frcond3  30876  nfrgr2v  30879  frgr3vlem1  30880  frgr3vlem2  30881  2pthfrgrrn  30889  frgrncvvdeqlem2  30907  shincli  31970  chincli  32068  lsmsnorb  33993  quslsm  34003  coinfliprv  35162  altxpsspw  36835  mnurndlem1  45359  fourierdlem103  47313  fourierdlem104  47314  nnsum3primes4  48980  isubgr3stgrlem6  49163  grlimprclnbgrvtx  49191  grlimgrtrilem2  49194  gpgprismgr4cycllem8  49294  pgnbgreunbgr  49317