Theorem prss 4758

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

Syntax hints:   ↔ wb 207   ∧ wa 396   ∈ wcel 2119  Vcvv 3432   ⊆ wss 3890  {cpr 4564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-ss 3907  df-sn 4563  df-pr 4565

This theorem is referenced by:  tpss  4775  uniintsn  4922  pwssun  5517  xpsspw  5759  dffv2  6929  fiint  9234  wunex2  10659  hashfun  14397  fun2dmnop0  14464  prdsle  17423  prdsless  17424  prdsleval  17438  pwsle  17454  acsfn2  17627  joinfval  18335  joindmss  18341  meetfval  18349  meetdmss  18355  clatl  18472  ipoval  18494  ipolerval  18496  eqgfval  19149  eqgval  19150  eqg0subg  19169  gaorb  19280  pmtrrn2  19433  efgcpbllema  19727  frgpuplem  19745  isnzr2hash  20498  thlle  21679  ltbval  22026  ltbwe  22027  opsrle  22030  opsrtoslem1  22038  isphtpc  24986  axlowdimlem4  29039  structgrssvtx  29118  structgrssiedg  29119  umgredg  29232  wlk1walk  29732  wlkonl1iedg  29757  wlkdlem2  29775  3wlkdlem6  30260  frcond2  30362  frcond3  30364  nfrgr2v  30367  frgr3vlem1  30368  frgr3vlem2  30369  2pthfrgrrn  30377  frgrncvvdeqlem2  30395  shincli  31458  chincli  31556  lsmsnorb  33481  quslsm  33495  coinfliprv  34674  altxpsspw  36212  mnurndlem1  44732  fourierdlem103  46659  fourierdlem104  46660  nnsum3primes4  48286  isubgr3stgrlem6  48469  grlimprclnbgrvtx  48497  grlimgrtrilem2  48500  gpgprismgr4cycllem8  48600  pgnbgreunbgr  48623