Theorem opexg 4370

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

Step	Hyp	Ref	Expression
1		dfopg 3902	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ⟨𝐴, 𝐵⟩ = {{𝐴}, {𝐴, 𝐵}})
2		elex 2833	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
3		snexg 4323	. . . . 5 ⊢ (𝐴 ∈ V → {𝐴} ∈ V)
4	2, 3	syl 14	. . . 4 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V)
5	4	adantr 276	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴} ∈ V)
6		elex 2833	. . . 4 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V)
7		prexg 4351	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ V)
8	2, 6, 7	syl2an 289	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V)
9		prexg 4351	. . 3 ⊢ (({𝐴} ∈ V ∧ {𝐴, 𝐵} ∈ V) → {{𝐴}, {𝐴, 𝐵}} ∈ V)
10	5, 8, 9	syl2anc 415	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {{𝐴}, {𝐴, 𝐵}} ∈ V)
11	1, 10	eqeltrd 2315	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ⟨𝐴, 𝐵⟩ ∈ V)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∈ wcel 2209  Vcvv 2821  {csn 3709  {cpr 3710  ⟨cop 3712

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4251  ax-pow 4313  ax-pr 4348

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718

This theorem is used by:  opex  4371  otexg  4372  opeliunxp  4832  opbrop  4856  relsnopg  4881  opswapg  5277  elxp4  5278  elxp5  5279  resfunexg  5939  fliftel  6002  fliftel1  6003  oprabid  6120  ovexg  6122  ovssunirng  6123  eloprabga  6178  op1st  6384  op2nd  6385  ot1stg  6390  ot2ndg  6391  ot3rdgg  6392  elxp6  6407  mpofvex  6445  algrflem  6469  algrflemg  6470  mpoxopoveq  6515  brtposg  6529  tfr0dm  6597  tfrlemisucaccv  6600  tfrlemibxssdm  6602  tfrlemibfn  6603  tfrlemi14d  6608  tfr1onlemsucaccv  6616  tfr1onlembxssdm  6618  tfr1onlembfn  6619  tfr1onlemres  6624  tfrcllemsucaccv  6629  tfrcllembxssdm  6631  tfrcllembfn  6632  tfrcllemres  6637  mapsnend  7104  en2prd  7111  fnfi  7255  snopfsuppdc  7305  djulclb  7402  inl11  7412  1stinl  7421  2ndinl  7422  1stinr  7423  2ndinr  7424  mulpipq2  7745  enq0breq  7810  addvalex  8218  peano2nnnn  8227  axcnre  8255  frec2uzrdg  10868  frecuzrdg0  10872  frecuzrdgg  10875  frecuzrdg0t  10881  zfz1isolem1  11315  s1leng  11415  s111  11422  pfxclz  11474  eucalgval2  12857  crth  13032  phimullem  13033  ennnfonelemp1  13356  setsvala  13442  setsex  13443  setsfun  13446  setsfun0  13447  setsresg  13449  setscom  13451  strslfv  13456  strslfv3  13457  setsslid  13462  bassetsnn  13468  strle1g  13520  1strbas  13531  2strbasg  13534  2stropg  13535  2strbas1g  13537  2strop1g  13538  rngbaseg  13550  rngplusgg  13551  rngmulrg  13552  srngbased  13561  srngplusgd  13562  srngmulrd  13563  srnginvld  13564  lmodbased  13579  lmodplusgd  13580  lmodscad  13581  lmodvscad  13582  ipsbased  13591  ipsaddgd  13592  ipsmulrd  13593  ipsscad  13594  ipsvscad  13595  ipsipd  13596  topgrpbasd  13611  topgrpplusgd  13612  topgrptsetd  13613  imasex  13686  imasival  13687  imasbas  13688  imasplusg  13689  imasmulr  13690  imasaddfnlemg  13695  imasaddvallemg  13696  xpsfval  13729  intopsn  13747  mgm1  13750  sgrp1  13786  mnd1  13822  mnd1id  13823  grp1  13971  grp1inv  13972  prdsex  14280  prdsval  14281  xpsval  14309  ring1  14472  psrval  15162  fnpsr  15163  psrbasg  15183  psrplusgg  15187  txlm  15517  struct2slots2dom  16496  structvtxval  16497  structiedg0val  16498  structgrssvtx  16500  structgrssiedg  16501  gropd  16505  edgopval  16520  edgstruct  16522  isuhgropm  16539  uhgrunop  16545  upgrop  16562  upgr0eop  16580  upgr1eopdc  16581  upgr1een  16582  umgr1een  16583  upgrunop  16585  umgrunop  16587  isuspgropen  16622  isusgropen  16623  ausgrusgrben  16626  usgr0eop  16700  uspgr1eopdc  16701  usgr1eop  16703  uhgrspanop  16740  vtxdgop  16750  p1evtxdeqfilem  16769  p1evtxdeqfi  16770  p1evtxdp1fi  16771  eupthvdres  16933  eupth2lem3fi  16934  konigsbergumgr  16945