Theorem rspc2ev 3585

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 3572	. . . 4 ⊢ ((𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑦 ∈ 𝐷 𝜒)
3	2	anim2i 625	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ (𝐵 ∈ 𝐷 ∧ 𝜓)) → (𝐴 ∈ 𝐶 ∧ ∃𝑦 ∈ 𝐷 𝜒))
4	3	3impb 1123	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → (𝐴 ∈ 𝐶 ∧ ∃𝑦 ∈ 𝐷 𝜒))
5		rspc2v.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
6	5	rexbidv 3176	. . 3 ⊢ (𝑥 = 𝐴 → (∃𝑦 ∈ 𝐷 𝜑 ↔ ∃𝑦 ∈ 𝐷 𝜒))
7	6	rspcev 3572	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ ∃𝑦 ∈ 𝐷 𝜒) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑)
8	4, 7	syl 17	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1095   = wceq 1550   ∈ wcel 2132  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-3an 1097  df-tru 1553  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-ral 3067  df-rex 3077

This theorem is referenced by:  2rspcedvdw  3586  opelxp  5672  fprb  7163  f1prex  7253  nf1const  7273  rspceov  7430  erov  8780  ralxpmap  8863  2dom  8996  elfiun  9362  dffi3  9363  ixpiunwdom  9524  1re  11167  hashdmpropge2  14482  wrdl2exs2  14945  ello12r  15516  ello1d  15522  elo12r  15527  o1lo1  15536  addcn2  15593  mulcn2  15595  bezoutlem3  16547  bezout  16549  pythagtriplem18  16840  pczpre  16855  pcdiv  16860  4sqlem3  16958  4sqlem4  16960  4sqlem12  16964  vdwlem1  16989  vdwlem6  16994  vdwlem8  16996  vdwlem12  17000  vdwlem13  17001  0ram  17028  ramz2  17032  cat1lem  18101  sgrp2rid2ex  18936  pmtr3ncom  19487  psgnunilem1  19505  irredn0  20440  isnzr2  20536  hausnei2  23382  cnhaus  23383  dishaus  23411  ordthauslem  23412  txuni2  23594  xkoopn  23618  txopn  23631  txdis  23661  txdis1cn  23664  pthaus  23667  txhaus  23676  tx1stc  23679  xkohaus  23682  regr1lem  23768  qustgplem  24150  methaus  24549  met2ndci  24551  metnrmlem3  24891  elplyr  26230  aaliou2b  26371  aaliou3lem9  26380  2irrexpq  26762  2irrexpqALT  26831  2sqlem2  27448  2sqlem8  27456  2sqlem11  27459  2sqb  27462  2sqnn0  27468  2sqnn  27469  pntibnd  27623  madecut  27942  mulsproplem12  28186  precsexlem11  28276  eucliddivs  28435  elz12si  28532  zz12s  28534  remulscllem1  28559  legov  28720  iscgrad  28946  f1otrge  29007  axsegconlem1  29053  axsegcon  29063  axpaschlem  29076  axlowdimlem6  29083  axlowdim1  29095  axlowdim2  29096  axeuclidlem  29098  umgrvad2edg  29349  wwlksnwwlksnon  30050  upgr4cycl4dv4e  30322  3cyclfrgrrn1  30422  4cycl2vnunb  30427  br8d  32749  lt2addrd  32891  xlt2addrd  32900  xrnarchi  33314  txomap  34075  tpr2rico  34153  qqhval2  34223  elsx  34435  br2base  34510  dya2iocnrect  34522  connpconn  35523  satfv1fvfmla1  35711  br8  36044  br4  36046  brsegle  36396  hilbert1.1  36442  nn0prpwlem  36620  knoppndvlem21  36908  poimirlem1  38058  itg2addnclem3  38110  cntotbnd  38233  smprngopr  38489  3dim2  40030  llni2  40074  lvoli3  40139  lvoli2  40143  islinei  40302  psubspi2N  40310  elpaddri  40364  eldioph2lem1  43279  diophin  43291  fphpdo  43332  irrapxlem3  43339  irrapxlem4  43340  pellexlem6  43349  pell1234qrreccl  43369  pell1234qrmulcl  43370  pell1234qrdich  43376  pell1qr1  43386  pellqrexplicit  43392  rmxycomplete  43432  dgraalem  43660  tfsconcatrev  43863  clsk3nimkb  44554  fourierdlem64  46682  rspceaov  47729  modn0mul  47895  ichnreuop  48016  prelspr  48030  reuopreuprim  48070  6gbe  48331  7gbow  48332  8gbe  48333  9gbo  48334  11gbo  48335  elbigo2r  49113  rrx2xpref1o  49278  inlinecirc02plem  49346  sepfsepc  49487  iscnrm3lem7  49498