Theorem prss 4774

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  Vcvv 3438   ⊆ wss 3905  {cpr 4581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-un 3910  df-ss 3922  df-sn 4580  df-pr 4582

This theorem is referenced by:  tpss  4791  uniintsn  4938  pwssun  5515  xpsspw  5756  dffv2  6922  fiint  9235  fiintOLD  9236  wunex2  10651  hashfun  14362  fun2dmnop0  14429  prdsle  17384  prdsless  17385  prdsleval  17399  pwsle  17414  acsfn2  17587  joinfval  18295  joindmss  18301  meetfval  18309  meetdmss  18315  clatl  18432  ipoval  18454  ipolerval  18456  eqgfval  19073  eqgval  19074  eqg0subg  19093  gaorb  19204  pmtrrn2  19357  efgcpbllema  19651  frgpuplem  19669  isnzr2hash  20422  thlle  21622  ltbval  21966  ltbwe  21967  opsrle  21970  opsrtoslem1  21978  isphtpc  24909  axlowdimlem4  28908  structgrssvtx  28987  structgrssiedg  28988  umgredg  29101  wlk1walk  29602  wlkonl1iedg  29627  wlkdlem2  29645  3wlkdlem6  30127  frcond2  30229  frcond3  30231  nfrgr2v  30234  frgr3vlem1  30235  frgr3vlem2  30236  2pthfrgrrn  30244  frgrncvvdeqlem2  30262  shincli  31324  chincli  31422  lsmsnorb  33341  quslsm  33355  coinfliprv  34453  altxpsspw  35953  mnurndlem1  44257  fourierdlem103  46194  fourierdlem104  46195  nnsum3primes4  47776  isubgr3stgrlem6  47959  grlimprclnbgrvtx  47987  grlimgrtrilem2  47990  gpgprismgr4cycllem8  48090  pgnbgreunbgr  48113