Theorem opexg 4158

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 3711	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ⟨𝐴, 𝐵⟩ = {{𝐴}, {𝐴, 𝐵}})
2		elex 2700	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
3		snexg 4116	. . . . 5 ⊢ (𝐴 ∈ V → {𝐴} ∈ V)
4	2, 3	syl 14	. . . 4 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V)
5	4	adantr 274	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴} ∈ V)
6		elex 2700	. . . 4 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V)
7		prexg 4141	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ V)
8	2, 6, 7	syl2an 287	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V)
9		prexg 4141	. . 3 ⊢ (({𝐴} ∈ V ∧ {𝐴, 𝐵} ∈ V) → {{𝐴}, {𝐴, 𝐵}} ∈ V)
10	5, 8, 9	syl2anc 409	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {{𝐴}, {𝐴, 𝐵}} ∈ V)
11	1, 10	eqeltrd 2217	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ⟨𝐴, 𝐵⟩ ∈ V)

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1481  Vcvv 2689  {csn 3532  {cpr 3533  ⟨cop 3535

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 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4054  ax-pow 4106  ax-pr 4139

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-un 3080  df-in 3082  df-ss 3089  df-pw 3517  df-sn 3538  df-pr 3539  df-op 3541

This theorem is referenced by:  opex  4159  otexg  4160  opeliunxp  4602  opbrop  4626  relsnopg  4651  opswapg  5033  elxp4  5034  elxp5  5035  resfunexg  5649  fliftel  5702  fliftel1  5703  oprabid  5811  ovexg  5813  eloprabga  5866  op1st  6052  op2nd  6053  ot1stg  6058  ot2ndg  6059  ot3rdgg  6060  elxp6  6075  mpofvex  6109  algrflem  6134  algrflemg  6135  mpoxopoveq  6145  brtposg  6159  tfr0dm  6227  tfrlemisucaccv  6230  tfrlemibxssdm  6232  tfrlemibfn  6233  tfrlemi14d  6238  tfr1onlemsucaccv  6246  tfr1onlembxssdm  6248  tfr1onlembfn  6249  tfr1onlemres  6254  tfrcllemsucaccv  6259  tfrcllembxssdm  6261  tfrcllembfn  6262  tfrcllemres  6267  fnfi  6833  djulclb  6948  inl11  6958  1stinl  6967  2ndinl  6968  1stinr  6969  2ndinr  6970  mulpipq2  7203  enq0breq  7268  addvalex  7676  peano2nnnn  7685  axcnre  7713  frec2uzrdg  10213  frecuzrdg0  10217  frecuzrdgg  10220  frecuzrdg0t  10226  zfz1isolem1  10615  eucalgval2  11770  crth  11936  phimullem  11937  ennnfonelemp1  11955  setsvala  12029  setsex  12030  setsfun  12033  setsfun0  12034  setsresg  12036  setscom  12038  strslfv  12042  setsslid  12048  strle1g  12088  1strbas  12097  2strbasg  12099  2stropg  12100  2strbas1g  12102  2strop1g  12103  rngbaseg  12114  rngplusgg  12115  rngmulrg  12116  srngbased  12121  srngplusgd  12122  srngmulrd  12123  srnginvld  12124  lmodbased  12132  lmodplusgd  12133  lmodscad  12134  lmodvscad  12135  ipsbased  12140  ipsaddgd  12141  ipsmulrd  12142  ipsscad  12143  ipsvscad  12144  ipsipd  12145  topgrpbasd  12150  topgrpplusgd  12151  topgrptsetd  12152  txlm  12487