Theorem 2rexbidv 3232

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

Hypothesis

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

Assertion

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

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

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

Proof of Theorem 2rexbidv

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∃wrex 3091

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

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3092

This theorem is used by:  f1oiso  7358  elrnmpog  7554  elrnmpo  7555  ralrnmpo  7558  ovelrn  7596  opiota  8062  omeu  8576  oeeui  8594  eroveu  8816  erov  8818  elfiun  9397  dffi3  9398  xpwdomg  9554  brdom7disj  10530  brdom6disj  10531  genpv  10999  genpelv  11000  axcnre  11164  supadd  12198  supmullem1  12200  supmullem2  12201  supmul  12202  01sqrexlem6  15322  ello1  15590  ello1mpt  15596  elo1  15601  lo1o1  15607  o1lo1  15612  bezoutlem1  16619  bezoutlem3  16621  bezoutlem4  16622  bezout  16623  pythagtriplem2  16899  pythagtriplem19  16915  pythagtrip  16916  pcval  16926  pceu  16928  pczpre  16929  pcdiv  16934  4sqlem2  17031  4sqlem3  17032  4sqlem4  17034  4sq  17046  vdwlem1  17063  vdwlem12  17074  vdwlem13  17075  vdwnnlem1  17077  vdwnnlem2  17078  vdwnnlem3  17079  vdwnn  17080  ramub2  17096  rami  17097  cat1lem  18175  cat1  18176  pgpfac1lem3  20193  lspprel  21265  znunit  21763  cayleyhamiltonALT  23098  hausnei  23535  isreg2  23584  txuni2  23773  txbas  23775  xkoopn  23797  txcls  23812  txcnpi  23816  txdis1cn  23843  txtube  23848  txcmplem1  23849  hausdiag  23853  tx1stc  23858  regr1lem2  23948  qustgplem  24329  met2ndci  24730  dyadmax  25808  i1fadd  25905  i1fmul  25906  elply  26403  2sqlem2  27633  2sqlem8  27641  2sqlem9  27642  2sqlem11  27644  elmade  28101  mulsval  28353  mulsval2lem  28354  mulsproplem9  28368  mulsproplem12  28371  sltmuls1  28391  sltmuls2  28392  mulsuniflem  28393  addsdilem2  28396  mulsasslem1  28407  mulsasslem2  28408  mulsunif2  28414  precsexlemcbv  28450  precsexlem9  28459  precsexlem11  28461  eucliddivs  28620  bdayfinbndcbv  28710  bdayfinbndlem1  28711  bdayfinbndlem2  28712  bdayfinbnd  28713  elz12s  28716  z12zsodd  28726  z12sge0  28727  remulscllem1  28744  istrkgld  28779  istrkg3ld  28781  axtgupdim2  28791  axtgeucl  28792  legov  28905  iscgra  29171  dfcgra2  29192  axsegconlem1  29322  axpasch  29346  axlowdim  29366  axeuclidlem  29367  nb3grpr  29790  upgr4cycl4dv4e  30607  vdgn1frgrv2  30718  fusgr2wsp2nb  30756  l2p  30902  br8d  33024  gsumwun  33460  constrsuc  34192  constrsslem  34195  constrconj  34199  constrllcllem  34206  constrlccllem  34207  constrcccllem  34208  constrcbvlem  34209  pstmval  34349  eulerpartlemgh  34833  eulerpartlemgs2  34835  cvmliftlem15  35827  cvmlift2lem10  35841  satf  35882  satfv0  35887  satfrnmapom  35899  satfv0fun  35900  satf0op  35906  sat1el2xp  35908  fmlafvel  35914  fmla1  35916  fmlaomn0  35919  gonan0  35921  goaln0  35922  gonar  35924  goalr  35926  fmlasucdisj  35928  satffunlem2lem1  35933  dmopab3rexdif  35934  satfv0fvfmla0  35942  sategoelfvb  35948  satfv1fvfmla1  35952  2goelgoanfmla1  35953  br8  36285  br6  36286  br4  36287  elaltxp  36504  brsegle  36637  ellines  36681  nn0prpwlem  36890  nn0prpw  36891  ptrest  38327  ismblfin  38369  itg2addnclem3  38381  itg2addnc  38382  releldmqscoss  39452  isline  40571  psubspi  40579  paddfval  40629  elpadd  40631  paddvaln0N  40633  3rspcedvd  43045  flt4lem7  43449  nna4b4nsq  43450  mzpcompact2lem  43540  mzpcompact2  43541  pell1qrval  43631  elpell1qr  43632  pell14qrval  43633  elpell14qr  43634  pell1234qrval  43635  elpell1234qr  43636  jm2.27  43793  expdiophlem1  43806  oenord1  44101  oaun3lem1  44159  clsk1independent  44830  limclner  46423  fourierdlem42  46921  fourierdlem48  46926  sprel  48291  prelspr  48293  prprelb  48323  prprelprb  48324  reuprpr  48330  isgbe  48574  isgbow  48575  isgbo  48576  sbgoldbalt  48604  sgoldbeven3prm  48606  mogoldbb  48608  sbgoldbo  48610  nnsum3primesle9  48617  usgrgrtrirex  48773  grlimgrtri  48826  grlimedgnedg  48954  bigoval  49386  elbigo  49388  iscnrm3r  49783  iscnrm3l  49786