ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  opexg GIF version

Theorem opexg 4150
Description: An ordered pair of sets is a set. (Contributed by Jim Kingdon, 11-Jan-2019.)
Assertion
Ref Expression
opexg ((𝐴𝑉𝐵𝑊) → ⟨𝐴, 𝐵⟩ ∈ V)

Proof of Theorem opexg
StepHypRef Expression
1 dfopg 3703 . 2 ((𝐴𝑉𝐵𝑊) → ⟨𝐴, 𝐵⟩ = {{𝐴}, {𝐴, 𝐵}})
2 elex 2697 . . . . 5 (𝐴𝑉𝐴 ∈ V)
3 snexg 4108 . . . . 5 (𝐴 ∈ V → {𝐴} ∈ V)
42, 3syl 14 . . . 4 (𝐴𝑉 → {𝐴} ∈ V)
54adantr 274 . . 3 ((𝐴𝑉𝐵𝑊) → {𝐴} ∈ V)
6 elex 2697 . . . 4 (𝐵𝑊𝐵 ∈ V)
7 prexg 4133 . . . 4 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ V)
82, 6, 7syl2an 287 . . 3 ((𝐴𝑉𝐵𝑊) → {𝐴, 𝐵} ∈ V)
9 prexg 4133 . . 3 (({𝐴} ∈ V ∧ {𝐴, 𝐵} ∈ V) → {{𝐴}, {𝐴, 𝐵}} ∈ V)
105, 8, 9syl2anc 408 . 2 ((𝐴𝑉𝐵𝑊) → {{𝐴}, {𝐴, 𝐵}} ∈ V)
111, 10eqeltrd 2216 1 ((𝐴𝑉𝐵𝑊) → ⟨𝐴, 𝐵⟩ ∈ V)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wcel 1480  Vcvv 2686  {csn 3527  {cpr 3528  cop 3530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sep 4046  ax-pow 4098  ax-pr 4131
This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-v 2688  df-un 3075  df-in 3077  df-ss 3084  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536
This theorem is referenced by:  opex  4151  otexg  4152  opeliunxp  4594  opbrop  4618  relsnopg  4643  opswapg  5025  elxp4  5026  elxp5  5027  resfunexg  5641  fliftel  5694  fliftel1  5695  oprabid  5803  ovexg  5805  eloprabga  5858  op1st  6044  op2nd  6045  ot1stg  6050  ot2ndg  6051  ot3rdgg  6052  elxp6  6067  mpofvex  6101  algrflem  6126  algrflemg  6127  mpoxopoveq  6137  brtposg  6151  tfr0dm  6219  tfrlemisucaccv  6222  tfrlemibxssdm  6224  tfrlemibfn  6225  tfrlemi14d  6230  tfr1onlemsucaccv  6238  tfr1onlembxssdm  6240  tfr1onlembfn  6241  tfr1onlemres  6246  tfrcllemsucaccv  6251  tfrcllembxssdm  6253  tfrcllembfn  6254  tfrcllemres  6259  fnfi  6825  djulclb  6940  inl11  6950  1stinl  6959  2ndinl  6960  1stinr  6961  2ndinr  6962  mulpipq2  7186  enq0breq  7251  addvalex  7659  peano2nnnn  7668  axcnre  7696  frec2uzrdg  10189  frecuzrdg0  10193  frecuzrdgg  10196  frecuzrdg0t  10202  zfz1isolem1  10590  eucalgval2  11741  crth  11907  phimullem  11908  ennnfonelemp1  11926  setsvala  12000  setsex  12001  setsfun  12004  setsfun0  12005  setsresg  12007  setscom  12009  strslfv  12013  setsslid  12019  strle1g  12059  1strbas  12068  2strbasg  12070  2stropg  12071  2strbas1g  12073  2strop1g  12074  rngbaseg  12085  rngplusgg  12086  rngmulrg  12087  srngbased  12092  srngplusgd  12093  srngmulrd  12094  srnginvld  12095  lmodbased  12103  lmodplusgd  12104  lmodscad  12105  lmodvscad  12106  ipsbased  12111  ipsaddgd  12112  ipsmulrd  12113  ipsscad  12114  ipsvscad  12115  ipsipd  12116  topgrpbasd  12121  topgrpplusgd  12122  topgrptsetd  12123  txlm  12458
  Copyright terms: Public domain W3C validator