Theorem rspc2ev 3635

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1540   ∈ wcel 2108  ∃wrex 3070

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071

This theorem is referenced by:  2rspcedvdw  3636  rspc3ev  3639  opelxp  5721  fprb  7214  f1prex  7304  nf1const  7324  rspceov  7480  erov  8854  ralxpmap  8936  2dom  9070  elfiun  9470  dffi3  9471  ixpiunwdom  9630  1re  11261  hashdmpropge2  14522  wrdl2exs2  14985  ello12r  15553  ello1d  15559  elo12r  15564  o1lo1  15573  addcn2  15630  mulcn2  15632  bezoutlem3  16578  bezout  16580  pythagtriplem18  16870  pczpre  16885  pcdiv  16890  4sqlem3  16988  4sqlem4  16990  4sqlem12  16994  vdwlem1  17019  vdwlem6  17024  vdwlem8  17026  vdwlem12  17030  vdwlem13  17031  0ram  17058  ramz2  17062  cat1lem  18141  sgrp2rid2ex  18940  pmtr3ncom  19493  psgnunilem1  19511  irredn0  20423  isnzr2  20518  hausnei2  23361  cnhaus  23362  dishaus  23390  ordthauslem  23391  txuni2  23573  xkoopn  23597  txopn  23610  txdis  23640  txdis1cn  23643  pthaus  23646  txhaus  23655  tx1stc  23658  xkohaus  23661  regr1lem  23747  qustgplem  24129  methaus  24533  met2ndci  24535  metnrmlem3  24883  elplyr  26240  aaliou2b  26383  aaliou3lem9  26392  2irrexpq  26773  2irrexpqALT  26843  2sqlem2  27462  2sqlem8  27470  2sqlem11  27473  2sqb  27476  2sqnn0  27482  2sqnn  27483  pntibnd  27637  madecut  27921  mulsproplem12  28153  precsexlem11  28241  zzs12  28423  remulscllem1  28432  legov  28593  iscgrad  28819  f1otrge  28880  axsegconlem1  28932  axsegcon  28942  axpaschlem  28955  axlowdimlem6  28962  axlowdim1  28974  axlowdim2  28975  axeuclidlem  28977  umgrvad2edg  29230  wwlksnwwlksnon  29935  upgr4cycl4dv4e  30204  3cyclfrgrrn1  30304  4cycl2vnunb  30309  br8d  32622  lt2addrd  32755  xlt2addrd  32762  xrnarchi  33191  txomap  33833  tpr2rico  33911  qqhval2  33983  elsx  34195  br2base  34271  dya2iocnrect  34283  connpconn  35240  satfv1fvfmla1  35428  br8  35756  br4  35758  brsegle  36109  hilbert1.1  36155  nn0prpwlem  36323  knoppndvlem21  36533  poimirlem1  37628  itg2addnclem3  37680  cntotbnd  37803  smprngopr  38059  3dim2  39470  llni2  39514  lvoli3  39579  lvoli2  39583  islinei  39742  psubspi2N  39750  elpaddri  39804  eldioph2lem1  42771  diophin  42783  fphpdo  42828  irrapxlem3  42835  irrapxlem4  42836  pellexlem6  42845  pell1234qrreccl  42865  pell1234qrmulcl  42866  pell1234qrdich  42872  pell1qr1  42882  pellqrexplicit  42888  rmxycomplete  42929  dgraalem  43157  tfsconcatrev  43361  clsk3nimkb  44053  fourierdlem64  46185  rspceaov  47209  ichnreuop  47459  prelspr  47473  reuopreuprim  47513  6gbe  47758  7gbow  47759  8gbe  47760  9gbo  47761  11gbo  47762  modn0mul  48441  elbigo2r  48474  rrx2xpref1o  48639  inlinecirc02plem  48707  sepfsepc  48825  iscnrm3lem7  48836