Theorem rspc2ev 3295

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∃wrex 2897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-v 3175

This theorem is referenced by:  rspc3ev  3297  opelxp  5070  f1prex  6439  rspceov  6590  erov  7731  ralxpmap  7793  2dom  7915  elfiun  8219  dffi3  8220  ixpiunwdom  8379  1re  9918  wrdl2exs2  13538  ello12r  14096  ello1d  14102  elo12r  14107  o1lo1  14116  addcn2  14172  mulcn2  14174  bezoutlem3  15096  bezout  15098  pythagtriplem18  15375  pczpre  15390  pcdiv  15395  4sqlem3  15492  4sqlem4  15494  4sqlem12  15498  vdwlem1  15523  vdwlem6  15528  vdwlem8  15530  vdwlem12  15534  vdwlem13  15535  0ram  15562  ramz2  15566  sgrp2rid2ex  17237  pmtr3ncom  17718  psgnunilem1  17736  irredn0  18526  isnzr2  19084  hausnei2  20967  cnhaus  20968  dishaus  20996  ordthauslem  20997  txuni2  21178  xkoopn  21202  txopn  21215  txdis  21245  txdis1cn  21248  pthaus  21251  txhaus  21260  tx1stc  21263  xkohaus  21266  regr1lem  21352  qustgplem  21734  methaus  22135  met2ndci  22137  metnrmlem3  22472  elplyr  23761  aaliou2b  23900  aaliou3lem9  23909  2sqlem2  24943  2sqlem8  24951  2sqlem11  24954  2sqb  24957  pntibnd  25082  legov  25280  iscgrad  25503  f1otrge  25552  axsegconlem1  25597  axsegcon  25607  axpaschlem  25620  axlowdimlem6  25627  axlowdim1  25639  axlowdim2  25640  axeuclidlem  25642  structgrssvtxlem  25700  upgredg  25811  el2wlksotot  26409  3cyclfrgrarn1  26539  4cycl2vnunb  26544  br8d  28802  lt2addrd  28903  xlt2addrd  28913  xrnarchi  29069  txomap  29229  tpr2rico  29286  qqhval2  29354  elsx  29584  isanmbfm  29645  br2base  29658  dya2iocnrect  29670  conpcon  30471  br8  30899  br4  30901  fprb  30916  brsegle  31385  hilbert1.1  31431  nn0prpwlem  31487  knoppndvlem21  31693  poimirlem1  32580  itg2addnclem3  32633  cntotbnd  32765  smprngopr  33021  3dim2  33772  llni2  33816  lvoli3  33881  lvoli2  33885  islinei  34044  psubspi2N  34052  elpaddri  34106  eldioph2lem1  36341  diophin  36354  fphpdo  36399  irrapxlem3  36406  irrapxlem4  36407  pellexlem6  36416  pell1234qrreccl  36436  pell1234qrmulcl  36437  pell1234qrdich  36443  pell1qr1  36453  pellqrexplicit  36459  rmxycomplete  36500  dgraalem  36734  clsk3nimkb  37358  fourierdlem64  39063  rspceaov  39926  6gbe  40193  7gbo  40194  8gbe  40195  9gboa  40196  11gboa  40197  umgrvad2edg  40440  wwlksnwwlksnon  41121  upgr4cycl4dv4e  41352  3cyclfrgrrn1  41455  4cycl2vnunb-av  41460  modn0mul  42109  elbigo2r  42145