Theorem rspc2ev 3549

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1089   = wceq 1543   ∈ wcel 2110  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1091  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066  df-rex 3067

This theorem is referenced by:  rspc3ev  3551  opelxp  5587  fprb  7009  f1prex  7094  nf1const  7114  rspceov  7260  erov  8496  ralxpmap  8577  2dom  8707  elfiun  9046  dffi3  9047  ixpiunwdom  9206  1re  10833  hashdmpropge2  14049  wrdl2exs2  14511  ello12r  15078  ello1d  15084  elo12r  15089  o1lo1  15098  addcn2  15155  mulcn2  15157  bezoutlem3  16101  bezout  16103  pythagtriplem18  16385  pczpre  16400  pcdiv  16405  4sqlem3  16503  4sqlem4  16505  4sqlem12  16509  vdwlem1  16534  vdwlem6  16539  vdwlem8  16541  vdwlem12  16545  vdwlem13  16546  0ram  16573  ramz2  16577  cat1lem  17602  sgrp2rid2ex  18354  pmtr3ncom  18867  psgnunilem1  18885  irredn0  19721  isnzr2  20301  hausnei2  22250  cnhaus  22251  dishaus  22279  ordthauslem  22280  txuni2  22462  xkoopn  22486  txopn  22499  txdis  22529  txdis1cn  22532  pthaus  22535  txhaus  22544  tx1stc  22547  xkohaus  22550  regr1lem  22636  qustgplem  23018  methaus  23418  met2ndci  23420  metnrmlem3  23758  elplyr  25095  aaliou2b  25234  aaliou3lem9  25243  2irrexpq  25618  2irrexpqALT  25683  2sqlem2  26299  2sqlem8  26307  2sqlem11  26310  2sqb  26313  2sqnn0  26319  2sqnn  26320  pntibnd  26474  legov  26676  iscgrad  26902  f1otrge  26963  axsegconlem1  27008  axsegcon  27018  axpaschlem  27031  axlowdimlem6  27038  axlowdim1  27050  axlowdim2  27051  axeuclidlem  27053  umgrvad2edg  27301  wwlksnwwlksnon  27999  upgr4cycl4dv4e  28268  3cyclfrgrrn1  28368  4cycl2vnunb  28373  br8d  30669  lt2addrd  30794  xlt2addrd  30801  xrnarchi  31157  txomap  31498  tpr2rico  31576  qqhval2  31644  elsx  31874  isanmbfm  31935  br2base  31948  dya2iocnrect  31960  connpconn  32910  satfv1fvfmla1  33098  br8  33442  br4  33444  madecut  33802  brsegle  34147  hilbert1.1  34193  nn0prpwlem  34248  knoppndvlem21  34449  poimirlem1  35515  itg2addnclem3  35567  cntotbnd  35691  smprngopr  35947  3dim2  37219  llni2  37263  lvoli3  37328  lvoli2  37332  islinei  37491  psubspi2N  37499  elpaddri  37553  2rspcedvdw  39903  eldioph2lem1  40285  diophin  40297  fphpdo  40342  irrapxlem3  40349  irrapxlem4  40350  pellexlem6  40359  pell1234qrreccl  40379  pell1234qrmulcl  40380  pell1234qrdich  40386  pell1qr1  40396  pellqrexplicit  40402  rmxycomplete  40442  dgraalem  40673  clsk3nimkb  41327  fourierdlem64  43386  rspceaov  44361  ichnreuop  44597  prelspr  44611  reuopreuprim  44651  6gbe  44896  7gbow  44897  8gbe  44898  9gbo  44899  11gbo  44900  modn0mul  45539  elbigo2r  45572  rrx2xpref1o  45737  inlinecirc02plem  45805  sepfsepc  45894  iscnrm3lem7  45906