Theorem opexg 4368

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 4321	. . . . 5 ⊢ (𝐴 ∈ V → {𝐴} ∈ V)
4	2, 3	syl 14	. . . 4 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V)
5	4	adantr 276	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴} ∈ V)
6		elex 2833	. . . 4 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V)
7		prexg 4349	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ V)
8	2, 6, 7	syl2an 289	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V)
9		prexg 4349	. . 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 4249  ax-pow 4311  ax-pr 4346

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  4369  otexg  4370  opeliunxp  4830  opbrop  4854  relsnopg  4879  opswapg  5274  elxp4  5275  elxp5  5276  resfunexg  5936  fliftel  5999  fliftel1  6000  oprabid  6117  ovexg  6119  ovssunirng  6120  eloprabga  6175  op1st  6380  op2nd  6381  ot1stg  6386  ot2ndg  6387  ot3rdgg  6388  elxp6  6403  mpofvex  6441  algrflem  6465  algrflemg  6466  mpoxopoveq  6511  brtposg  6525  tfr0dm  6593  tfrlemisucaccv  6596  tfrlemibxssdm  6598  tfrlemibfn  6599  tfrlemi14d  6604  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfr1onlemres  6620  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllembfn  6628  tfrcllemres  6633  mapsnend  7099  en2prd  7106  fnfi  7250  snopfsuppdc  7299  djulclb  7395  inl11  7405  1stinl  7414  2ndinl  7415  1stinr  7416  2ndinr  7417  mulpipq2  7738  enq0breq  7803  addvalex  8211  peano2nnnn  8220  axcnre  8248  frec2uzrdg  10846  frecuzrdg0  10850  frecuzrdgg  10853  frecuzrdg0t  10859  zfz1isolem1  11292  s1leng  11392  s111  11399  pfxclz  11451  eucalgval2  12831  crth  13002  phimullem  13003  ennnfonelemp1  13297  setsvala  13383  setsex  13384  setsfun  13387  setsfun0  13388  setsresg  13390  setscom  13392  strslfv  13397  strslfv3  13398  setsslid  13403  bassetsnn  13409  strle1g  13460  1strbas  13471  2strbasg  13474  2stropg  13475  2strbas1g  13477  2strop1g  13478  rngbaseg  13490  rngplusgg  13491  rngmulrg  13492  srngbased  13501  srngplusgd  13502  srngmulrd  13503  srnginvld  13504  lmodbased  13519  lmodplusgd  13520  lmodscad  13521  lmodvscad  13522  ipsbased  13531  ipsaddgd  13532  ipsmulrd  13533  ipsscad  13534  ipsvscad  13535  ipsipd  13536  topgrpbasd  13551  topgrpplusgd  13552  topgrptsetd  13553  imasex  13626  imasival  13627  imasbas  13628  imasplusg  13629  imasmulr  13630  imasaddfnlemg  13635  imasaddvallemg  13636  xpsfval  13669  intopsn  13687  mgm1  13690  sgrp1  13726  mnd1  13762  mnd1id  13763  grp1  13911  grp1inv  13912  prdsex  14172  prdsval  14173  xpsval  14201  ring1  14364  psrval  15050  fnpsr  15051  psrbasg  15065  psrplusgg  15069  txlm  15380  struct2slots2dom  16283  structvtxval  16284  structiedg0val  16285  structgrssvtx  16287  structgrssiedg  16288  gropd  16292  edgopval  16307  edgstruct  16309  isuhgropm  16326  uhgrunop  16332  upgrop  16349  upgr0eop  16367  upgr1eopdc  16368  upgr1een  16369  umgr1een  16370  upgrunop  16372  umgrunop  16374  isuspgropen  16409  isusgropen  16410  ausgrusgrben  16413  usgr0eop  16487  uspgr1eopdc  16488  usgr1eop  16490  uhgrspanop  16527  vtxdgop  16537  p1evtxdeqfilem  16556  p1evtxdeqfi  16557  p1evtxdp1fi  16558  eupthvdres  16720  eupth2lem3fi  16721  konigsbergumgr  16732