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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

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

This theorem is used by:  2rspcedvdw  3589  opelxp  5683  fprb  7187  f1prex  7280  nf1const  7300  rspceov  7457  erov  8813  ralxpmap  8902  2dom  9036  elfiun  9400  dffi3  9401  ixpiunwdom  9562  1re  11279  hashdmpropge2  14595  wrdl2exs2  15064  ello12r  15651  ello1d  15657  elo12r  15662  o1lo1  15671  addcn2  15728  mulcn2  15730  bezoutlem3  16678  bezout  16680  pythagtriplem18  16971  pczpre  16986  pcdiv  16991  4sqlem3  17089  4sqlem4  17091  4sqlem12  17095  vdwlem1  17120  vdwlem6  17125  vdwlem8  17127  vdwlem12  17131  vdwlem13  17132  0ram  17159  ramz2  17163  cat1lem  18232  sgrp2rid2ex  19087  pmtr3ncom  19650  psgnunilem1  19668  irredn0  20614  isnzr2  20729  hausnei2  23632  cnhaus  23633  dishaus  23661  ordthauslem  23662  txuni2  23845  xkoopn  23869  txopn  23882  txdis  23912  txdis1cn  23915  pthaus  23918  txhaus  23927  tx1stc  23930  xkohaus  23933  regr1lem  24019  qustgplem  24401  methaus  24800  met2ndci  24802  metnrmlem3  25142  elplyr  26480  aaliou2b  26631  aaliou3lem9  26640  2irrexpq  27022  2irrexpqALT  27091  2sqlem2  27708  2sqlem8  27716  2sqlem11  27719  2sqb  27722  2sqnn  27729  pntibnd  27883  madecut  28202  mulsproplem12  28446  precsexlem11  28536  eucliddivs  28695  elz12si  28792  zz12s  28794  remulscllem1  28819  legov  28981  iscgrad  29251  f1otrge  29382  axsegconlem1  29428  axsegcon  29438  axpaschlem  29451  axlowdimlem6  29458  axlowdim1  29470  axlowdim2  29471  axeuclidlem  29473  umgrvad2edg  29727  wwlksnwwlksnon  30437  upgr4cycl4dv4e  30719  3cyclfrgrrn1  30819  4cycl2vnunb  30824  br8d  33135  lt2addrd  33275  xlt2addrd  33284  xrnarchi  33678  txomap  34399  tpr2rico  34477  qqhval2  34547  elsx  34760  br2base  34835  dya2iocnrect  34847  connpconn  35921  satfv1fvfmla1  36109  br8  36442  br4  36444  brsegle  36795  hilbert1.1  36841  nn0prpwlem  37032  knoppndvlem21  37320  poimirlem1  38459  itg2addnclem3  38511  cntotbnd  38650  smprngopr  38906  3dim2  40445  llni2  40489  lvoli3  40554  lvoli2  40558  islinei  40717  psubspi2N  40725  elpaddri  40779  eldioph2lem1  43709  diophin  43721  fphpdo  43762  irrapxlem3  43769  irrapxlem4  43770  pellexlem6  43779  pell1234qrreccl  43799  pell1234qrmulcl  43800  pell1234qrdich  43806  pell1qr1  43816  pellqrexplicit  43822  rmxycomplete  43862  dgraalem  44090  tfsconcatrev  44293  clsk3nimkb  44984  fourierdlem64  47102  rspceaov  48189  modn0mul  48355  ichnreuop  48476  prelspr  48490  reuopreuprim  48530  6gbe  48791  7gbow  48792  8gbe  48793  9gbo  48794  11gbo  48795  smprngprmrng  49358  elbigo2r  49587  rrx2xpref1o  49752  inlinecirc02plem  49820  sepfsepc  49958  iscnrm3lem7  49969