Theorem prss 4816

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

Syntax hints:   ↔ wb 205   ∧ wa 396   ∈ wcel 2106  Vcvv 3473   ⊆ wss 3944  {cpr 4624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-un 3949  df-in 3951  df-ss 3961  df-sn 4623  df-pr 4625

This theorem is referenced by:  tpss  4831  uniintsn  4984  pwssun  5564  xpsspw  5801  dffv2  6972  fiint  9307  wunex2  10715  hashfun  14379  fun2dmnop0  14437  prdsle  17390  prdsless  17391  prdsleval  17405  pwsle  17420  acsfn2  17589  joinfval  18308  joindmss  18314  meetfval  18322  meetdmss  18328  clatl  18443  ipoval  18465  ipolerval  18467  eqgfval  19028  eqgval  19029  gaorb  19137  pmtrrn2  19292  efgcpbllema  19586  frgpuplem  19604  isnzr2hash  20248  thlle  21184  thlleOLD  21185  ltbval  21526  ltbwe  21527  opsrle  21530  opsrtoslem1  21544  isphtpc  24439  axlowdimlem4  28068  structgrssvtx  28149  structgrssiedg  28150  umgredg  28263  wlk1walk  28761  wlkonl1iedg  28787  wlkdlem2  28805  3wlkdlem6  29283  frcond2  29385  frcond3  29387  nfrgr2v  29390  frgr3vlem1  29391  frgr3vlem2  29392  2pthfrgrrn  29400  frgrncvvdeqlem2  29418  shincli  30478  chincli  30576  lsmsnorb  32359  quslsm  32374  coinfliprv  33310  altxpsspw  34777  mnurndlem1  42809  fourierdlem103  44696  fourierdlem104  44697  nnsum3primes4  46226