Theorem rspc2ev 3601

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054

This theorem is referenced by:  2rspcedvdw  3602  rspc3ev  3605  opelxp  5674  fprb  7168  f1prex  7259  nf1const  7279  rspceov  7436  erov  8787  ralxpmap  8869  2dom  9001  elfiun  9381  dffi3  9382  ixpiunwdom  9543  1re  11174  hashdmpropge2  14448  wrdl2exs2  14912  ello12r  15483  ello1d  15489  elo12r  15494  o1lo1  15503  addcn2  15560  mulcn2  15562  bezoutlem3  16511  bezout  16513  pythagtriplem18  16803  pczpre  16818  pcdiv  16823  4sqlem3  16921  4sqlem4  16923  4sqlem12  16927  vdwlem1  16952  vdwlem6  16957  vdwlem8  16959  vdwlem12  16963  vdwlem13  16964  0ram  16991  ramz2  16995  cat1lem  18058  sgrp2rid2ex  18854  pmtr3ncom  19405  psgnunilem1  19423  irredn0  20332  isnzr2  20427  hausnei2  23240  cnhaus  23241  dishaus  23269  ordthauslem  23270  txuni2  23452  xkoopn  23476  txopn  23489  txdis  23519  txdis1cn  23522  pthaus  23525  txhaus  23534  tx1stc  23537  xkohaus  23540  regr1lem  23626  qustgplem  24008  methaus  24408  met2ndci  24410  metnrmlem3  24750  elplyr  26106  aaliou2b  26249  aaliou3lem9  26258  2irrexpq  26640  2irrexpqALT  26710  2sqlem2  27329  2sqlem8  27337  2sqlem11  27340  2sqb  27343  2sqnn0  27349  2sqnn  27350  pntibnd  27504  madecut  27794  mulsproplem12  28030  precsexlem11  28119  eucliddivs  28265  zzs12  28339  remulscllem1  28351  legov  28512  iscgrad  28738  f1otrge  28799  axsegconlem1  28844  axsegcon  28854  axpaschlem  28867  axlowdimlem6  28874  axlowdim1  28886  axlowdim2  28887  axeuclidlem  28889  umgrvad2edg  29140  wwlksnwwlksnon  29845  upgr4cycl4dv4e  30114  3cyclfrgrrn1  30214  4cycl2vnunb  30219  br8d  32538  lt2addrd  32674  xlt2addrd  32682  xrnarchi  33138  txomap  33824  tpr2rico  33902  qqhval2  33972  elsx  34184  br2base  34260  dya2iocnrect  34272  connpconn  35222  satfv1fvfmla1  35410  br8  35743  br4  35745  brsegle  36096  hilbert1.1  36142  nn0prpwlem  36310  knoppndvlem21  36520  poimirlem1  37615  itg2addnclem3  37667  cntotbnd  37790  smprngopr  38046  3dim2  39462  llni2  39506  lvoli3  39571  lvoli2  39575  islinei  39734  psubspi2N  39742  elpaddri  39796  eldioph2lem1  42748  diophin  42760  fphpdo  42805  irrapxlem3  42812  irrapxlem4  42813  pellexlem6  42822  pell1234qrreccl  42842  pell1234qrmulcl  42843  pell1234qrdich  42849  pell1qr1  42859  pellqrexplicit  42865  rmxycomplete  42906  dgraalem  43134  tfsconcatrev  43337  clsk3nimkb  44029  fourierdlem64  46168  rspceaov  47198  modn0mul  47358  ichnreuop  47473  prelspr  47487  reuopreuprim  47527  6gbe  47772  7gbow  47773  8gbe  47774  9gbo  47775  11gbo  47776  elbigo2r  48542  rrx2xpref1o  48707  inlinecirc02plem  48775  sepfsepc  48916  iscnrm3lem7  48927