Theorem prss 4784

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  Vcvv 3447   ⊆ wss 3914  {cpr 4591

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 3449  df-un 3919  df-ss 3931  df-sn 4590  df-pr 4592

This theorem is referenced by:  tpss  4801  uniintsn  4949  pwssun  5530  xpsspw  5772  dffv2  6956  fiint  9277  fiintOLD  9278  wunex2  10691  hashfun  14402  fun2dmnop0  14469  prdsle  17425  prdsless  17426  prdsleval  17440  pwsle  17455  acsfn2  17624  joinfval  18332  joindmss  18338  meetfval  18346  meetdmss  18352  clatl  18467  ipoval  18489  ipolerval  18491  eqgfval  19108  eqgval  19109  eqg0subg  19128  gaorb  19239  pmtrrn2  19390  efgcpbllema  19684  frgpuplem  19702  isnzr2hash  20428  thlle  21606  ltbval  21950  ltbwe  21951  opsrle  21954  opsrtoslem1  21962  isphtpc  24893  axlowdimlem4  28872  structgrssvtx  28951  structgrssiedg  28952  umgredg  29065  wlk1walk  29567  wlkonl1iedg  29593  wlkdlem2  29611  3wlkdlem6  30094  frcond2  30196  frcond3  30198  nfrgr2v  30201  frgr3vlem1  30202  frgr3vlem2  30203  2pthfrgrrn  30211  frgrncvvdeqlem2  30229  shincli  31291  chincli  31389  lsmsnorb  33362  quslsm  33376  coinfliprv  34474  altxpsspw  35965  mnurndlem1  44270  fourierdlem103  46207  fourierdlem104  46208  nnsum3primes4  47789  isubgr3stgrlem6  47970  grlimgrtrilem2  47994  gpgprismgr4cycllem8  48092  pgnbgreunbgr  48115