Theorem rspc2ev 3634

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1536   ∈ wcel 2105  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068

This theorem is referenced by:  2rspcedvdw  3635  rspc3ev  3638  opelxp  5724  fprb  7213  f1prex  7303  nf1const  7323  rspceov  7479  erov  8852  ralxpmap  8934  2dom  9068  elfiun  9467  dffi3  9468  ixpiunwdom  9627  1re  11258  hashdmpropge2  14518  wrdl2exs2  14981  ello12r  15549  ello1d  15555  elo12r  15560  o1lo1  15569  addcn2  15626  mulcn2  15628  bezoutlem3  16574  bezout  16576  pythagtriplem18  16865  pczpre  16880  pcdiv  16885  4sqlem3  16983  4sqlem4  16985  4sqlem12  16989  vdwlem1  17014  vdwlem6  17019  vdwlem8  17021  vdwlem12  17025  vdwlem13  17026  0ram  17053  ramz2  17057  cat1lem  18149  sgrp2rid2ex  18952  pmtr3ncom  19507  psgnunilem1  19525  irredn0  20439  isnzr2  20534  hausnei2  23376  cnhaus  23377  dishaus  23405  ordthauslem  23406  txuni2  23588  xkoopn  23612  txopn  23625  txdis  23655  txdis1cn  23658  pthaus  23661  txhaus  23670  tx1stc  23673  xkohaus  23676  regr1lem  23762  qustgplem  24144  methaus  24548  met2ndci  24550  metnrmlem3  24896  elplyr  26254  aaliou2b  26397  aaliou3lem9  26406  2irrexpq  26787  2irrexpqALT  26857  2sqlem2  27476  2sqlem8  27484  2sqlem11  27487  2sqb  27490  2sqnn0  27496  2sqnn  27497  pntibnd  27651  madecut  27935  mulsproplem12  28167  precsexlem11  28255  zzs12  28437  remulscllem1  28446  legov  28607  iscgrad  28833  f1otrge  28894  axsegconlem1  28946  axsegcon  28956  axpaschlem  28969  axlowdimlem6  28976  axlowdim1  28988  axlowdim2  28989  axeuclidlem  28991  umgrvad2edg  29244  wwlksnwwlksnon  29944  upgr4cycl4dv4e  30213  3cyclfrgrrn1  30313  4cycl2vnunb  30318  br8d  32629  lt2addrd  32761  xlt2addrd  32768  xrnarchi  33173  txomap  33794  tpr2rico  33872  qqhval2  33944  elsx  34174  br2base  34250  dya2iocnrect  34262  connpconn  35219  satfv1fvfmla1  35407  br8  35735  br4  35737  brsegle  36089  hilbert1.1  36135  nn0prpwlem  36304  knoppndvlem21  36514  poimirlem1  37607  itg2addnclem3  37659  cntotbnd  37782  smprngopr  38038  3dim2  39450  llni2  39494  lvoli3  39559  lvoli2  39563  islinei  39722  psubspi2N  39730  elpaddri  39784  eldioph2lem1  42747  diophin  42759  fphpdo  42804  irrapxlem3  42811  irrapxlem4  42812  pellexlem6  42821  pell1234qrreccl  42841  pell1234qrmulcl  42842  pell1234qrdich  42848  pell1qr1  42858  pellqrexplicit  42864  rmxycomplete  42905  dgraalem  43133  tfsconcatrev  43337  clsk3nimkb  44029  fourierdlem64  46125  rspceaov  47146  ichnreuop  47396  prelspr  47410  reuopreuprim  47450  6gbe  47695  7gbow  47696  8gbe  47697  9gbo  47698  11gbo  47699  modn0mul  48369  elbigo2r  48402  rrx2xpref1o  48567  inlinecirc02plem  48635  sepfsepc  48723  iscnrm3lem7  48735