Theorem prss 4780

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  Vcvv 3444   ⊆ wss 3911  {cpr 4587

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 3446  df-un 3916  df-ss 3928  df-sn 4586  df-pr 4588

This theorem is referenced by:  tpss  4797  uniintsn  4945  pwssun  5523  xpsspw  5763  dffv2  6938  fiint  9253  fiintOLD  9254  wunex2  10667  hashfun  14378  fun2dmnop0  14445  prdsle  17401  prdsless  17402  prdsleval  17416  pwsle  17431  acsfn2  17600  joinfval  18308  joindmss  18314  meetfval  18322  meetdmss  18328  clatl  18443  ipoval  18465  ipolerval  18467  eqgfval  19084  eqgval  19085  eqg0subg  19104  gaorb  19215  pmtrrn2  19366  efgcpbllema  19660  frgpuplem  19678  isnzr2hash  20404  thlle  21582  ltbval  21926  ltbwe  21927  opsrle  21930  opsrtoslem1  21938  isphtpc  24869  axlowdimlem4  28848  structgrssvtx  28927  structgrssiedg  28928  umgredg  29041  wlk1walk  29542  wlkonl1iedg  29567  wlkdlem2  29585  3wlkdlem6  30067  frcond2  30169  frcond3  30171  nfrgr2v  30174  frgr3vlem1  30175  frgr3vlem2  30176  2pthfrgrrn  30184  frgrncvvdeqlem2  30202  shincli  31264  chincli  31362  lsmsnorb  33335  quslsm  33349  coinfliprv  34447  altxpsspw  35938  mnurndlem1  44243  fourierdlem103  46180  fourierdlem104  46181  nnsum3primes4  47762  isubgr3stgrlem6  47943  grlimgrtrilem2  47967  gpgprismgr4cycllem8  48065  pgnbgreunbgr  48088