Theorem rexbidva 3177

Description: Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 9-Mar-1997.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 6-Dec-2019.) (Proof shortened by Wolf Lammen, 10-Dec-2019.)

Hypothesis

Ref	Expression
ralbidva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
rexbidva	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem rexbidva

Step	Hyp	Ref	Expression
1		ralbidva.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
2	1	pm5.32da 579	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒)))
3	2	rexbidv2 3175	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2108  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3071

This theorem is referenced by:  rexbidv  3179  2rexbiia  3218  2rexbidva  3220  rexeqbidva  3333  frinxp  5768  onfr  6423  dfimafn  6971  funimass4  6973  fliftel  7329  fliftf  7335  isomin  7357  f1oiso  7371  releldm2  8068  oaass  8599  eldifsucnn  8702  cofonr  8712  naddunif  8731  qsinxp  8833  qliftel  8840  fimaxg  9323  ordunifi  9326  supisolem  9513  fiming  9538  wemapwe  9737  ttrcltr  9756  ttrclse  9767  frmin  9789  cflim2  10303  cfsmolem  10310  alephsing  10316  brdom7disj  10571  brdom6disj  10572  alephreg  10622  nqereu  10969  1idpr  11069  map2psrpr  11150  axsup  11336  rereccl  11985  sup3  12225  infm3  12227  supadd  12236  creur  12260  creui  12261  nndiv  12312  nnrecl  12524  rpnnen1lem2  13019  rpnnen1lem1  13020  rpnnen1lem3  13021  rpnnen1lem5  13023  supxrbnd1  13363  supxrbnd2  13364  supxrbnd  13370  rabssnn0fi  14027  mptnn0fsupp  14038  expnlbnd  14272  wrdl3s3  15001  limsuplt  15515  clim2  15540  clim2c  15541  clim0c  15543  ello12  15552  elo12  15563  rlimresb  15601  climabs0  15621  sumeq2ii  15729  mertens  15922  prodeq2ii  15947  zprod  15973  nndivides  16300  alzdvds  16357  oddm1even  16380  oddnn02np1  16385  oddge22np1  16386  evennn02n  16387  evennn2n  16388  divalglem4  16433  divalgb  16441  modremain  16445  modprmn0modprm0  16845  vdwlem6  17024  vdwlem11  17029  vdw  17032  ramval  17046  imasleval  17586  dfiso3  17817  fullestrcsetc  18196  fullsetcestrc  18211  isipodrs  18582  ipodrsfi  18584  gsumpropd2lem  18692  mndpropd  18772  grppropd  18969  qus0subgbas  19216  conjnmzb  19271  symgextfo  19440  symgfixfo  19457  sylow1lem2  19617  sylow3lem1  19645  sylow3lem3  19647  lsmelvalm  19669  lsmass  19687  iscyg3  19904  ghmcyg  19914  cycsubgcyg  19919  pgpfac1lem2  20095  pgpfac1lem4  20098  ablfac2  20109  dvdsr02  20372  crngunit  20378  dvdsrpropd  20416  rngqiprngimfo  21311  lpigen  21345  pzriprnglem10  21501  znunit  21582  elfilspd  21823  psdmul  22170  scmatmats  22517  symgmatr01  22660  isclo  23095  iscnp3  23252  lmbrf  23268  cncnp  23288  lmss  23306  isnrm2  23366  cmpfi  23416  1stcfb  23453  1stccnp  23470  ptrescn  23647  txkgen  23660  xkoinjcn  23695  trfil3  23896  fmid  23968  lmflf  24013  txflf  24014  ptcmplem3  24062  tsmsf1o  24153  ucnprima  24291  metrest  24537  metcnp  24554  metcnp2  24555  txmetcnp  24560  metuel2  24578  metustbl  24579  psmetutop  24580  metucn  24584  evth2  24992  lmmbrf  25296  iscfil2  25300  fmcfil  25306  iscau2  25311  iscau4  25313  iscauf  25314  caucfil  25317  iscmet3lem3  25324  cfilresi  25329  causs  25332  lmclim  25337  ivth2  25490  ovolfioo  25502  ovolficc  25503  ovolshftlem1  25544  ovolscalem1  25548  volsup2  25640  ismbf3d  25689  mbfaddlem  25695  mbfsup  25699  mbfinf  25700  itg2seq  25777  itg2gt0  25795  ellimc2  25912  ellimc3  25914  rolle  26028  cmvth  26029  cmvthOLD  26030  mvth  26031  dvlip  26032  dvivth  26049  lhop1lem  26052  deg1ldg  26131  ulm2  26428  ulmdvlem3  26445  dcubic  26889  mcubic  26890  cubic2  26891  rlimcnp  27008  ftalem3  27118  isppw2  27158  lgsquadlem2  27425  2lgslem1a  27435  dchrmusumlema  27537  dchrisum0lema  27558  cofcutr  27958  lrrecfr  27976  addsrid  27997  addscom  27999  addsuniflem  28034  addsass  28038  addsbday  28050  negsunif  28087  mulsrid  28139  mulsasslem3  28191  n0s0suc  28345  renegscl  28430  readdscl  28431  remulscllem2  28433  remulscl  28434  tglowdim2l  28658  mirreu3  28662  oppcom  28752  iscgra1  28818  axsegcon  28942  axpasch  28956  axcontlem7  28985  usgr2pth0  29785  usgr2wspthon  29985  elwwlks2  29986  elwspths2spth  29987  rusgrnumwwlks  29994  clwwlkfo  30069  eclclwwlkn1  30094  eucrctshift  30262  fusgreg2wsp  30355  nmobndi  30794  nmounbi  30795  nmoo0  30810  h2hcau  30998  h2hlm  30999  shsel3  31334  pjhtheu2  31435  chscllem2  31657  adjbdln  32102  branmfn  32124  pjimai  32195  chrelati  32383  cdj3lem3  32457  cdj3lem3b  32459  dfimafnf  32646  ofpreima  32675  isarchi2  33192  submarchi  33193  archirng  33195  archiabl  33205  isarchiofld  33347  ellspds  33396  dvdsruasso2  33414  lsmssass  33430  grplsm0l  33431  fedgmullem2  33681  elirng  33736  zarcls  33873  ordtconnlem1  33923  lmdvg  33952  esumfsup  34071  dya2icoseg2  34280  eulerpartlemgh  34380  ballotlemodife  34500  ballotlemsima  34518  nummin  35105  erdszelem10  35205  iscvm  35264  wsuclem  35826  seglelin  36117  outsideofeu  36132  opnrebl  36321  opnrebl2  36322  filnetlem4  36382  bj-finsumval0  37286  phpreu  37611  ptrest  37626  poimirlem3  37630  poimirlem4  37631  poimirlem17  37644  poimirlem26  37653  poimirlem27  37654  broucube  37661  mblfinlem1  37664  lmclim2  37765  caures  37767  isbnd3b  37792  heiborlem7  37824  heiborlem10  37827  rrncmslem  37839  isdrngo2  37965  erimeq2  38679  prter3  38883  islshpsm  38981  lsatfixedN  39010  lrelat  39015  eqlkr2  39101  lshpkrlem1  39111  lfl1dim  39122  eqlkr4  39166  ishlat3N  39355  hlsupr2  39389  hlrelat5N  39403  hlrelat  39404  cvrval5  39417  cvrat42  39446  athgt  39458  3dim0  39459  islln3  39512  llnexatN  39523  islpln3  39535  islvol3  39578  islvol5  39581  isline4N  39779  polval2N  39908  4atex3  40083  cdleme0ex2N  40226  cdlemefrs29cpre1  40400  cdlemb3  40608  cdlemg33c  40710  cdlemg33e  40712  dia1dim2  41064  cdlemm10N  41120  dib1dim2  41170  diclspsn  41196  dih1dimatlem  41331  dihatexv2  41341  djhcvat42  41417  dihjat1lem  41430  dvh4dimat  41440  dvh2dimatN  41442  lcfrlem9  41552  mapdval4N  41634  mapdcv  41662  ef11d  42375  cxp112d  42377  cxp111d  42378  sn-sup3d  42502  fimgmcyc  42544  infdesc  42653  elrfirn  42706  elrfirn2  42707  mrefg3  42719  diophin  42783  diophun  42784  diophren  42824  rmxycomplete  42929  wepwsolem  43054  fnwe2lem2  43063  islssfg  43082  unielss  43230  onmaxnelsup  43235  onsupnmax  43240  onsupeqnmax  43259  tfsconcat0i  43358  ntrneineine0lem  44096  ntrneineine1lem  44097  ntrneiel2  44099  extoimad  44177  grumnudlem  44304  modelac8prim  45009  supsubc  45364  infxrbnd2  45380  supminfxr  45475  evthiccabs  45509  elicores  45546  clim2f  45651  clim2cf  45665  clim0cf  45669  clim2f2  45685  limsupub  45719  limsupmnflem  45735  limsupre2lem  45739  limsuplt2  45768  liminfreuzlem  45817  liminfltlem  45819  liminflimsupclim  45822  xlimmnfmpt  45858  xlimpnfmpt  45859  fourierdlem73  46194  fourierdlem83  46204  meaiuninc3v  46499  ovolval2  46659  cfsetsnfsetfo  47072  dfaimafn  47177  iccelpart  47420  sprsymrelf  47482  sprsymrelfo  47484  fmtnoprmfac1  47552  fmtnoprmfac2  47554  fmtnofac2lem  47555  dfeven2  47636  dfodd3  47637  dfvopnbgr2  47839  usgrgrtrirex  47917  stgredgiun  47925  uspgrsprfo  48064  elbigo2  48473  rrxlinesc  48656  rrxlinec  48657  rrx2line  48661  rrx2vlinest  48662  itsclquadeu  48698