Theorem 2rexbidv 3228

Description: Formula-building rule for restricted existential quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.)

Hypothesis

Ref	Expression
2rexbidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
2rexbidv	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒))

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜓(𝑥,𝑦)   𝜒(𝑥,𝑦)   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)

Proof of Theorem 2rexbidv

Step	Hyp	Ref	Expression
1		2rexbidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	rexbidv 3225	. 2 ⊢ (𝜑 → (∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒))
3	2	rexbidv 3225	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 205  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-rex 3069

This theorem is referenced by:  f1oiso  7202  elrnmpog  7387  elrnmpo  7388  ralrnmpo  7390  ovelrn  7426  opiota  7872  omeu  8378  oeeui  8395  eroveu  8559  erov  8561  elfiun  9119  dffi3  9120  xpwdomg  9274  brdom7disj  10218  brdom6disj  10219  genpv  10686  genpelv  10687  axcnre  10851  supadd  11873  supmullem1  11875  supmullem2  11876  supmul  11877  sqrlem6  14887  ello1  15152  ello1mpt  15158  elo1  15163  lo1o1  15169  o1lo1  15174  bezoutlem1  16175  bezoutlem3  16177  bezoutlem4  16178  bezout  16179  pythagtriplem2  16446  pythagtriplem19  16462  pythagtrip  16463  pcval  16473  pceu  16475  pczpre  16476  pcdiv  16481  4sqlem2  16578  4sqlem3  16579  4sqlem4  16581  4sq  16593  vdwlem1  16610  vdwlem12  16621  vdwlem13  16622  vdwnnlem1  16624  vdwnnlem2  16625  vdwnnlem3  16626  vdwnn  16627  ramub2  16643  rami  16644  cat1lem  17727  cat1  17728  pgpfac1lem3  19595  lspprel  20271  znunit  20683  cayleyhamiltonALT  21948  hausnei  22387  isreg2  22436  txuni2  22624  txbas  22626  xkoopn  22648  txcls  22663  txcnpi  22667  txdis1cn  22694  txtube  22699  txcmplem1  22700  hausdiag  22704  tx1stc  22709  regr1lem2  22799  qustgplem  23180  met2ndci  23584  dyadmax  24667  i1fadd  24764  i1fmul  24765  elply  25261  2sqlem2  26471  2sqlem8  26479  2sqlem9  26480  2sqlem11  26482  istrkgld  26724  istrkg3ld  26726  axtgupdim2  26736  axtgeucl  26737  legov  26850  iscgra  27074  dfcgra2  27095  axsegconlem1  27188  axpasch  27212  axlowdim  27232  axeuclidlem  27233  nb3grpr  27652  upgr4cycl4dv4e  28450  vdgn1frgrv2  28561  fusgr2wsp2nb  28599  l2p  28742  br8d  30851  pstmval  31747  eulerpartlemgh  32245  eulerpartlemgs2  32247  cvmliftlem15  33160  cvmlift2lem10  33174  satf  33215  satfv0  33220  satfrnmapom  33232  satfv0fun  33233  satf0op  33239  sat1el2xp  33241  fmlafvel  33247  fmla1  33249  fmlaomn0  33252  gonan0  33254  goaln0  33255  gonar  33257  goalr  33259  fmlasucdisj  33261  satffunlem2lem1  33266  dmopab3rexdif  33267  satfv0fvfmla0  33275  sategoelfvb  33281  satfv1fvfmla1  33285  2goelgoanfmla1  33286  br8  33629  br6  33630  br4  33631  elmade  33978  elaltxp  34204  brsegle  34337  ellines  34381  nn0prpwlem  34438  nn0prpw  34439  ptrest  35703  ismblfin  35745  itg2addnclem3  35757  itg2addnc  35758  releldmqscoss  36699  isline  37680  psubspi  37688  paddfval  37738  elpadd  37740  paddvaln0N  37742  3rspcedvd  40110  flt4lem7  40412  nna4b4nsq  40413  mzpcompact2lem  40489  mzpcompact2  40490  sbc4rexgOLD  40528  pell1qrval  40584  elpell1qr  40585  pell14qrval  40586  elpell14qr  40587  pell1234qrval  40588  elpell1234qr  40589  jm2.27  40746  expdiophlem1  40759  clsk1independent  41545  limclner  43082  fourierdlem42  43580  fourierdlem48  43585  sprel  44824  prelspr  44826  prprelb  44856  prprelprb  44857  reuprpr  44863  isgbe  45091  isgbow  45092  isgbo  45093  sbgoldbalt  45121  sgoldbeven3prm  45123  mogoldbb  45125  sbgoldbo  45127  nnsum3primesle9  45134  bigoval  45783  elbigo  45785  iscnrm3r  46130  iscnrm3l  46133