Theorem 2rexbidv 3231

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 3190	. 2 ⊢ (𝜑 → (∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒))
3	2	rexbidv 3190	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒))

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

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 1945

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

This theorem is used by:  f1oiso  7390  elrnmpog  7587  elrnmpo  7588  ralrnmpo  7591  ovelrn  7629  mpt3fvd  7720  opiota  8105  omeu  8631  oeeui  8649  eroveu  8871  erov  8873  elfiun  9459  dffi3  9460  xpwdomg  9616  brdom7disj  10649  brdom6disj  10650  genpv  11123  genpelv  11124  axcnre  11288  supadd  12325  supmullem1  12327  supmullem2  12328  supmul  12329  01sqrexlem6  15457  ello1  15726  ello1mpt  15732  elo1  15737  lo1o1  15743  o1lo1  15748  bezoutlem1  16756  bezoutlem3  16758  bezoutlem4  16759  bezout  16760  pythagtriplem2  17039  pythagtriplem19  17055  pythagtrip  17056  pcval  17066  pceu  17068  pczpre  17069  pcdiv  17074  4sqlem2  17171  4sqlem3  17172  4sqlem4  17174  4sq  17186  vdwlem1  17203  vdwlem12  17214  vdwlem13  17215  vdwnnlem1  17217  vdwnnlem2  17218  vdwnnlem3  17219  vdwnn  17220  ramub2  17236  rami  17237  cat1lem  18321  cat1  18322  pgpfac1lem3  20344  lspprel  21420  znunit  21924  cayleyhamiltonALT  23264  hausnei  23701  isreg2  23750  txuni2  23939  txbas  23941  xkoopn  23963  txcls  23978  txcnpi  23982  txdis1cn  24009  txtube  24014  txcmplem1  24015  hausdiag  24019  tx1stc  24024  regr1lem2  24114  qustgplem  24495  met2ndci  24896  dyadmax  25974  i1fadd  26071  i1fmul  26072  elply  26568  2sqlem2  27802  2sqlem8  27810  2sqlem9  27811  2sqlem11  27813  flt4lem7  28046  nna4b4nsq  28047  elmade  28300  mulsval  28552  mulsval2lem  28553  mulsproplem9  28567  mulsproplem12  28570  sltmuls1  28590  sltmuls2  28591  mulsuniflem  28592  addsdilem2  28595  mulsasslem1  28606  mulsasslem2  28607  mulsunif2  28613  precsexlemcbv  28649  precsexlem9  28658  precsexlem11  28660  eucliddivs  28819  bdayfinbndcbv  28909  bdayfinbndlem1  28910  bdayfinbndlem2  28911  bdayfinbnd  28912  elz12s  28915  z12zsodd  28925  z12sge0  28926  remulscllem1  28943  istrkgld  28978  istrkg3ld  28980  axtgupdim2  28990  axtgeucl  28991  legov  29105  iscgra  29373  dfcgra2  29395  axsegconlem1  29552  axpasch  29576  axlowdim  29596  axeuclidlem  29597  nb3grpr  30020  upgr4cycl4dv4e  30843  vdgn1frgrv2  30954  fusgr2wsp2nb  30992  l2p  31138  br8d  33300  gsumwun  33736  edomediv  33955  constrsuc  34481  constrsslem  34484  constrconj  34488  constrllcllem  34495  constrlccllem  34496  constrcccllem  34497  constrcbvlem  34498  pstmval  34638  eulerpartlemgh  35121  eulerpartlemgs2  35123  omeueq  35837  cvmliftlem15  36271  cvmlift2lem10  36285  satf  36326  satfv0  36331  satfrnmapom  36343  satfv0fun  36344  satf0op  36350  sat1el2xp  36352  fmlafvel  36358  fmla1  36360  fmlaomn0  36363  gonan0  36365  goaln0  36366  gonar  36368  goalr  36370  fmlasucdisj  36372  satffunlem2lem1  36377  dmopab3rexdif  36378  satfv0fvfmla0  36386  sategoelfvb  36392  satfv1fvfmla1  36396  2goelgoanfmla1  36397  br8  36736  br6  36737  br4  36738  elaltxp  36955  brsegle  37088  ellines  37132  nn0prpwlem  37325  nn0prpw  37326  ptrest  38805  ismblfin  38847  itg2addnclem3  38859  itg2addnc  38860  releldmqscoss  39943  isline  41062  psubspi  41070  paddfval  41120  elpadd  41122  paddvaln0N  41124  3rspcedvd  43537  mzpcompact2lem  44028  mzpcompact2  44029  pell1qrval  44119  elpell1qr  44120  pell14qrval  44121  elpell14qr  44122  pell1234qrval  44123  elpell1234qr  44124  jm2.27  44281  expdiophlem1  44294  oenord1  44579  oaun3lem1  44637  clsk1independent  45307  limclner  46934  fourierdlem42  47432  fourierdlem48  47437  sprel  48839  prelspr  48841  prprelb  48871  prprelprb  48872  reuprpr  48878  isgbe  49122  isgbow  49123  isgbo  49124  sbgoldbalt  49152  sgoldbeven3prm  49154  mogoldbb  49156  sbgoldbo  49158  nnsum3primesle9  49165  usgrgrtrirex  49321  grlimgrtri  49374  grlimedgnedg  49502  lazval  49725  ellaz  49726  bigoval  49992  elbigo  49994  iscnrm3r  50393  iscnrm3l  50396  fuconuniqex2  51118