Theorem rspc2ev 3517

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

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384   ∧ w3a 1100   = wceq 1637   ∈ wcel 2156  ∃wrex 3097

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-rex 3102  df-v 3393

This theorem is referenced by:  rspc3ev  3519  opelxp  5346  f1prex  6763  rspceov  6920  erov  8080  ralxpmap  8144  2dom  8265  elfiun  8575  dffi3  8576  ixpiunwdom  8735  1re  10325  hashdmpropge2  13482  wrdl2exs2  13915  ello12r  14471  ello1d  14477  elo12r  14482  o1lo1  14491  addcn2  14547  mulcn2  14549  bezoutlem3  15477  bezout  15479  pythagtriplem18  15754  pczpre  15769  pcdiv  15774  4sqlem3  15871  4sqlem4  15873  4sqlem12  15877  vdwlem1  15902  vdwlem6  15907  vdwlem8  15909  vdwlem12  15913  vdwlem13  15914  0ram  15941  ramz2  15945  sgrp2rid2ex  17619  pmtr3ncom  18096  psgnunilem1  18114  irredn0  18905  isnzr2  19472  hausnei2  21371  cnhaus  21372  dishaus  21400  ordthauslem  21401  txuni2  21582  xkoopn  21606  txopn  21619  txdis  21649  txdis1cn  21652  pthaus  21655  txhaus  21664  tx1stc  21667  xkohaus  21670  regr1lem  21756  qustgplem  22137  methaus  22538  met2ndci  22540  metnrmlem3  22877  elplyr  24171  aaliou2b  24310  aaliou3lem9  24319  2sqlem2  25357  2sqlem8  25365  2sqlem11  25368  2sqb  25371  pntibnd  25496  legov  25694  iscgrad  25917  f1otrge  25966  axsegconlem1  26011  axsegcon  26021  axpaschlem  26034  axlowdimlem6  26041  axlowdim1  26053  axlowdim2  26054  axeuclidlem  26056  structgrssvtxlemOLD  26129  umgrvad2edg  26320  wwlksnwwlksnon  27053  wwlksnwwlksnonOLD  27055  upgr4cycl4dv4e  27358  3cyclfrgrrn1  27460  4cycl2vnunb  27465  br8d  29747  lt2addrd  29843  xlt2addrd  29850  xrnarchi  30063  txomap  30226  tpr2rico  30283  qqhval2  30351  elsx  30582  isanmbfm  30643  br2base  30656  dya2iocnrect  30668  connpconn  31540  br8  31968  br4  31970  fprb  31991  brsegle  32536  hilbert1.1  32582  nn0prpwlem  32638  knoppndvlem21  32840  poimirlem1  33723  itg2addnclem3  33775  cntotbnd  33906  smprngopr  34162  3dim2  35248  llni2  35292  lvoli3  35357  lvoli2  35361  islinei  35520  psubspi2N  35528  elpaddri  35582  eldioph2lem1  37825  diophin  37838  fphpdo  37883  irrapxlem3  37890  irrapxlem4  37891  pellexlem6  37900  pell1234qrreccl  37920  pell1234qrmulcl  37921  pell1234qrdich  37927  pell1qr1  37937  pellqrexplicit  37943  rmxycomplete  37983  dgraalem  38216  clsk3nimkb  38838  fourierdlem64  40866  rspceaov  41786  6gbe  42234  7gbow  42235  8gbe  42236  9gbo  42237  11gbo  42238  prelspr  42304  modn0mul  42883  elbigo2r  42915