Theorem prss 4781

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-ss 3916  df-sn 4585  df-pr 4587

This theorem is used by:  tpss  4797  uniintsn  4945  pwssun  5547  xpsspw  5790  dffv2  6973  fiint  9296  wunex2  10747  hashfun  14502  fun2dmnop0  14569  prdsle  17547  prdsless  17548  prdsleval  17562  pwsle  17578  acsfn2  17751  joinfval  18459  joindmss  18465  meetfval  18473  meetdmss  18479  clatl  18596  ipoval  18618  ipolerval  18620  eqgfval  19301  eqgval  19302  eqg0subg  19324  gaorb  19434  pmtrrn2  19587  efgcpbllema  19881  frgpuplem  19899  isnzr2hash  20680  thlle  21910  ltbval  22259  ltbwe  22260  opsrle  22263  opsrtoslem1  22271  isphtpc  25222  axlowdimlem4  29402  structgrssvtx  29481  structgrssiedg  29482  umgredg  29595  wlk1walk  30098  wlkonl1iedg  30123  wlkdlem2  30141  3wlkdlem6  30645  frcond2  30747  frcond3  30749  nfrgr2v  30752  frgr3vlem1  30753  frgr3vlem2  30754  2pthfrgrrn  30762  frgrncvvdeqlem2  30780  shincli  31843  chincli  31941  lsmsnorb  33824  quslsm  33834  coinfliprv  34994  altxpsspw  36557  mnurndlem1  45105  fourierdlem103  47037  fourierdlem104  47038  nnsum3primes4  48704  isubgr3stgrlem6  48887  grlimprclnbgrvtx  48915  grlimgrtrilem2  48918  gpgprismgr4cycllem8  49018  pgnbgreunbgr  49041