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  10848  frecuzrdg0  10852  frecuzrdgg  10855  frecuzrdg0t  10861  zfz1isolem1  11294  s1leng  11394  s111  11401  pfxclz  11453  eucalgval2  12833  crth  13004  phimullem  13005  ennnfonelemp1  13299  setsvala  13385  setsex  13386  setsfun  13389  setsfun0  13390  setsresg  13392  setscom  13394  strslfv  13399  strslfv3  13400  setsslid  13405  bassetsnn  13411  strle1g  13462  1strbas  13473  2strbasg  13476  2stropg  13477  2strbas1g  13479  2strop1g  13480  rngbaseg  13492  rngplusgg  13493  rngmulrg  13494  srngbased  13503  srngplusgd  13504  srngmulrd  13505  srnginvld  13506  lmodbased  13521  lmodplusgd  13522  lmodscad  13523  lmodvscad  13524  ipsbased  13533  ipsaddgd  13534  ipsmulrd  13535  ipsscad  13536  ipsvscad  13537  ipsipd  13538  topgrpbasd  13553  topgrpplusgd  13554  topgrptsetd  13555  imasex  13628  imasival  13629  imasbas  13630  imasplusg  13631  imasmulr  13632  imasaddfnlemg  13637  imasaddvallemg  13638  xpsfval  13671  intopsn  13689  mgm1  13692  sgrp1  13728  mnd1  13764  mnd1id  13765  grp1  13913  grp1inv  13914  prdsex  14174  prdsval  14175  xpsval  14203  ring1  14366  psrval  15052  fnpsr  15053  psrbasg  15067  psrplusgg  15071  txlm  15382  struct2slots2dom  16291  structvtxval  16292  structiedg0val  16293  structgrssvtx  16295  structgrssiedg  16296  gropd  16300  edgopval  16315  edgstruct  16317  isuhgropm  16334  uhgrunop  16340  upgrop  16357  upgr0eop  16375  upgr1eopdc  16376  upgr1een  16377  umgr1een  16378  upgrunop  16380  umgrunop  16382  isuspgropen  16417  isusgropen  16418  ausgrusgrben  16421  usgr0eop  16495  uspgr1eopdc  16496  usgr1eop  16498  uhgrspanop  16535  vtxdgop  16545  p1evtxdeqfilem  16564  p1evtxdeqfi  16565  p1evtxdp1fi  16566  eupthvdres  16728  eupth2lem3fi  16729  konigsbergumgr  16740