Theorem prss 4845

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2108  Vcvv 3488   ⊆ wss 3976  {cpr 4650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993  df-sn 4649  df-pr 4651

This theorem is referenced by:  tpss  4862  uniintsn  5009  pwssun  5590  xpsspw  5833  dffv2  7017  fiint  9394  fiintOLD  9395  wunex2  10807  hashfun  14486  fun2dmnop0  14553  prdsle  17522  prdsless  17523  prdsleval  17537  pwsle  17552  acsfn2  17721  joinfval  18443  joindmss  18449  meetfval  18457  meetdmss  18463  clatl  18578  ipoval  18600  ipolerval  18602  eqgfval  19216  eqgval  19217  eqg0subg  19236  gaorb  19347  pmtrrn2  19502  efgcpbllema  19796  frgpuplem  19814  isnzr2hash  20545  thlle  21739  thlleOLD  21740  ltbval  22084  ltbwe  22085  opsrle  22088  opsrtoslem1  22102  isphtpc  25045  axlowdimlem4  28978  structgrssvtx  29059  structgrssiedg  29060  umgredg  29173  wlk1walk  29675  wlkonl1iedg  29701  wlkdlem2  29719  3wlkdlem6  30197  frcond2  30299  frcond3  30301  nfrgr2v  30304  frgr3vlem1  30305  frgr3vlem2  30306  2pthfrgrrn  30314  frgrncvvdeqlem2  30332  shincli  31394  chincli  31492  lsmsnorb  33384  quslsm  33398  coinfliprv  34447  altxpsspw  35941  mnurndlem1  44250  fourierdlem103  46130  fourierdlem104  46131  nnsum3primes4  47662  grlimgrtrilem2  47819