Theorem prss 4496

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

Syntax hints:   ↔ wb 196   ∧ wa 383   ∈ wcel 2139  Vcvv 3340   ⊆ wss 3715  {cpr 4323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-un 3720  df-in 3722  df-ss 3729  df-sn 4322  df-pr 4324

This theorem is referenced by:  tpss  4513  uniintsn  4666  pwssun  5170  xpsspw  5389  dffv2  6434  fpr2g  6640  fiint  8404  wunex2  9772  hashfun  13436  fun2dmnop0  13488  prdsle  16344  prdsless  16345  prdsleval  16359  pwsle  16374  acsfn2  16545  joinfval  17222  joindmss  17228  meetfval  17236  meetdmss  17242  clatl  17337  ipoval  17375  ipolerval  17377  eqgfval  17863  eqgval  17864  gaorb  17960  pmtrrn2  18100  efgcpbllema  18387  frgpuplem  18405  drngnidl  19451  drnglpir  19475  isnzr2hash  19486  ltbval  19693  ltbwe  19694  opsrle  19697  opsrtoslem1  19706  thlle  20263  isphtpc  23014  axlowdimlem4  26045  structgrssvtx  26133  structgrssiedg  26134  structgrssvtxlemOLD  26135  structgrssvtxOLD  26136  structgrssiedgOLD  26137  umgredg  26253  wlk1walk  26766  wlkonl1iedg  26792  wlkdlem2  26811  3wlkdlem6  27338  frcond2  27442  frcond3  27444  nfrgr2v  27447  frgr3vlem1  27448  frgr3vlem2  27449  2pthfrgrrn  27457  frgrncvvdeqlem2  27475  shincli  28551  chincli  28649  coinfliprv  30874  altxpsspw  32411  fourierdlem103  40947  fourierdlem104  40948  nnsum3primes4  42204