Theorem rspc2ev 3588

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.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
2	1	rexbidv 3186	. 2 ⊢ (𝑥 = 𝐴 → (∃𝑦 ∈ 𝐷 𝜑 ↔ ∃𝑦 ∈ 𝐷 𝜒))
3		simp1 1154	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → 𝐴 ∈ 𝐶)
4		rspc2v.2	. . . 4 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))
5	4	rspcev 3576	. . 3 ⊢ ((𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑦 ∈ 𝐷 𝜒)
6	5	3adant1 1148	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑦 ∈ 𝐷 𝜒)
7	2, 3, 6	rspcedvdw 3579	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087

This theorem is used by:  2rspcedvdw  3589  opelxp  5686  fprb  7199  f1prex  7292  nf1const  7312  rspceov  7469  erov  8835  ralxpmap  8924  2dom  9058  elfiun  9422  dffi3  9423  ixpiunwdom  9584  1re  11308  hashdmpropge2  14628  wrdl2exs2  15097  ello12r  15684  ello1d  15690  elo12r  15695  o1lo1  15704  addcn2  15761  mulcn2  15763  bezoutlem3  16714  bezout  16716  pythagtriplem18  17010  pczpre  17025  pcdiv  17030  4sqlem3  17128  4sqlem4  17130  4sqlem12  17134  vdwlem1  17159  vdwlem6  17164  vdwlem8  17166  vdwlem12  17170  vdwlem13  17171  0ram  17198  ramz2  17202  cat1lem  18271  sgrp2rid2ex  19126  pmtr3ncom  19689  psgnunilem1  19707  irredn0  20653  isnzr2  20768  hausnei2  23671  cnhaus  23672  dishaus  23700  ordthauslem  23701  txuni2  23884  xkoopn  23908  txopn  23921  txdis  23951  txdis1cn  23954  pthaus  23957  txhaus  23966  tx1stc  23969  xkohaus  23972  regr1lem  24058  qustgplem  24440  methaus  24839  met2ndci  24841  metnrmlem3  25181  elplyr  26519  aaliou2b  26668  aaliou3lem9  26677  2irrexpq  27059  2irrexpqALT  27128  2sqlem2  27745  2sqlem8  27753  2sqlem11  27756  2sqb  27759  2sqnn  27766  pntibnd  27920  madecut  28269  mulsproplem12  28513  precsexlem11  28603  eucliddivs  28762  elz12si  28859  zz12s  28861  remulscllem1  28886  legov  29048  iscgrad  29318  f1otrge  29449  axsegconlem1  29495  axsegcon  29505  axpaschlem  29518  axlowdimlem6  29525  axlowdim1  29537  axlowdim2  29538  axeuclidlem  29540  umgrvad2edg  29794  wwlksnwwlksnon  30504  upgr4cycl4dv4e  30786  3cyclfrgrrn1  30886  4cycl2vnunb  30891  br8d  33244  lt2addrd  33384  xlt2addrd  33393  xrnarchi  33787  txomap  34508  tpr2rico  34586  qqhval2  34656  elsx  34869  br2base  34943  dya2iocnrect  34955  connpconn  36042  satfv1fvfmla1  36230  br8  36563  br4  36565  brsegle  36915  hilbert1.1  36961  nn0prpwlem  37152  knoppndvlem21  37440  poimirlem1  38582  itg2addnclem3  38634  cntotbnd  38773  smprngopr  39029  3dim2  40568  llni2  40612  lvoli3  40677  lvoli2  40681  islinei  40840  psubspi2N  40848  elpaddri  40902  eldioph2lem1  43814  diophin  43826  fphpdo  43867  irrapxlem3  43874  irrapxlem4  43875  pellexlem6  43884  pell1234qrreccl  43904  pell1234qrmulcl  43905  pell1234qrdich  43911  pell1qr1  43921  pellqrexplicit  43927  rmxycomplete  43967  dgraalem  44190  tfsconcatrev  44393  clsk3nimkb  45083  fourierdlem64  47223  rspceaov  48310  modn0mul  48476  ichnreuop  48597  prelspr  48611  reuopreuprim  48651  6gbe  48912  7gbow  48913  8gbe  48914  9gbo  48915  11gbo  48916  smprngprmrng  49479  elbigo2r  49708  rrx2xpref1o  49873  inlinecirc02plem  49941  sepfsepc  50079  iscnrm3lem7  50090