Theorem rspc2ev 3588

Description: 2-variable restricted existential specialization, using implicit substitution. (Contributed by NM, 16-Oct-1999.)

Hypotheses

Ref	Expression
rspc2v.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
rspc2v.2	⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))

Assertion

Ref	Expression
rspc2ev	⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑)

Distinct variable groups:   𝑥,𝑦,𝐴   𝑦,𝐵   𝑥,𝐶   𝑥,𝐷,𝑦   𝜒,𝑥   𝜓,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥)   𝜒(𝑦)   𝐵(𝑥)   𝐶(𝑦)

Proof of Theorem rspc2ev

Step	Hyp	Ref	Expression
1		rspc2v.2	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))
2	1	rspcev 3575	. . . 4 ⊢ ((𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑦 ∈ 𝐷 𝜒)
3	2	anim2i 617	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ (𝐵 ∈ 𝐷 ∧ 𝜓)) → (𝐴 ∈ 𝐶 ∧ ∃𝑦 ∈ 𝐷 𝜒))
4	3	3impb 1114	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → (𝐴 ∈ 𝐶 ∧ ∃𝑦 ∈ 𝐷 𝜒))
5		rspc2v.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
6	5	rexbidv 3154	. . 3 ⊢ (𝑥 = 𝐴 → (∃𝑦 ∈ 𝐷 𝜑 ↔ ∃𝑦 ∈ 𝐷 𝜒))
7	6	rspcev 3575	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ ∃𝑦 ∈ 𝐷 𝜒) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑)
8	4, 7	syl 17	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2110  ∃wrex 3054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055

This theorem is referenced by:  2rspcedvdw  3589  rspc3ev  3592  opelxp  5650  fprb  7123  f1prex  7213  nf1const  7233  rspceov  7390  erov  8733  ralxpmap  8815  2dom  8947  elfiun  9309  dffi3  9310  ixpiunwdom  9471  1re  11104  hashdmpropge2  14382  wrdl2exs2  14845  ello12r  15416  ello1d  15422  elo12r  15427  o1lo1  15436  addcn2  15493  mulcn2  15495  bezoutlem3  16444  bezout  16446  pythagtriplem18  16736  pczpre  16751  pcdiv  16756  4sqlem3  16854  4sqlem4  16856  4sqlem12  16860  vdwlem1  16885  vdwlem6  16890  vdwlem8  16892  vdwlem12  16896  vdwlem13  16897  0ram  16924  ramz2  16928  cat1lem  17995  sgrp2rid2ex  18827  pmtr3ncom  19380  psgnunilem1  19398  irredn0  20334  isnzr2  20426  hausnei2  23261  cnhaus  23262  dishaus  23290  ordthauslem  23291  txuni2  23473  xkoopn  23497  txopn  23510  txdis  23540  txdis1cn  23543  pthaus  23546  txhaus  23555  tx1stc  23558  xkohaus  23561  regr1lem  23647  qustgplem  24029  methaus  24428  met2ndci  24430  metnrmlem3  24770  elplyr  26126  aaliou2b  26269  aaliou3lem9  26278  2irrexpq  26660  2irrexpqALT  26730  2sqlem2  27349  2sqlem8  27357  2sqlem11  27360  2sqb  27363  2sqnn0  27369  2sqnn  27370  pntibnd  27524  madecut  27821  mulsproplem12  28059  precsexlem11  28148  eucliddivs  28294  zzs12  28378  remulscllem1  28395  legov  28556  iscgrad  28782  f1otrge  28843  axsegconlem1  28888  axsegcon  28898  axpaschlem  28911  axlowdimlem6  28918  axlowdim1  28930  axlowdim2  28931  axeuclidlem  28933  umgrvad2edg  29184  wwlksnwwlksnon  29886  upgr4cycl4dv4e  30155  3cyclfrgrrn1  30255  4cycl2vnunb  30260  br8d  32581  lt2addrd  32724  xlt2addrd  32732  xrnarchi  33143  txomap  33837  tpr2rico  33915  qqhval2  33985  elsx  34197  br2base  34272  dya2iocnrect  34284  connpconn  35247  satfv1fvfmla1  35435  br8  35768  br4  35770  brsegle  36121  hilbert1.1  36167  nn0prpwlem  36335  knoppndvlem21  36545  poimirlem1  37640  itg2addnclem3  37692  cntotbnd  37815  smprngopr  38071  3dim2  39486  llni2  39530  lvoli3  39595  lvoli2  39599  islinei  39758  psubspi2N  39766  elpaddri  39820  eldioph2lem1  42772  diophin  42784  fphpdo  42829  irrapxlem3  42836  irrapxlem4  42837  pellexlem6  42846  pell1234qrreccl  42866  pell1234qrmulcl  42867  pell1234qrdich  42873  pell1qr1  42883  pellqrexplicit  42889  rmxycomplete  42929  dgraalem  43157  tfsconcatrev  43360  clsk3nimkb  44052  fourierdlem64  46187  rspceaov  47207  modn0mul  47367  ichnreuop  47482  prelspr  47496  reuopreuprim  47536  6gbe  47781  7gbow  47782  8gbe  47783  9gbo  47784  11gbo  47785  elbigo2r  48564  rrx2xpref1o  48729  inlinecirc02plem  48797  sepfsepc  48938  iscnrm3lem7  48949