Theorem rexbidva 3256

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
rexbidva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))

Assertion

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

Distinct variable group:   𝜑,𝑥

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

Proof of Theorem rexbidva

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∈ wcel 2079  ∃wrex 3104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1760  df-rex 3109

This theorem is referenced by:  rexbidv  3257  2rexbiia  3258  2rexbidva  3259  rexeqbidva  3383  frinxp  5512  onfr  6097  dfimafn  6588  funimass4  6590  fliftel  6916  fliftf  6922  isomin  6944  f1oiso  6958  releldm2  7589  oaass  8028  qsinxp  8214  qliftel  8221  fimaxg  8601  ordunifi  8604  supisolem  8773  fiming  8798  wemapwe  8995  cflim2  9520  cfsmolem  9527  alephsing  9533  brdom7disj  9788  brdom6disj  9789  alephreg  9839  nqereu  10186  1idpr  10286  map2psrpr  10367  axsup  10552  rereccl  11195  sup3  11435  infm3  11437  supadd  11446  creur  11469  creui  11470  nndiv  11520  nnrecl  11732  rpnnen1lem2  12215  rpnnen1lem1  12216  rpnnen1lem3  12217  rpnnen1lem5  12219  supxrbnd1  12553  supxrbnd2  12554  supxrbnd  12560  rabssnn0fi  13192  mptnn0fsupp  13203  expnlbnd  13432  wrdl3s3  14148  limsuplt  14658  clim2  14683  clim2c  14684  clim0c  14686  ello12  14695  elo12  14706  rlimresb  14744  climabs0  14764  sumeq2ii  14871  mertens  15063  prodeq2ii  15088  zprod  15112  nndivides  15438  alzdvds  15491  oddm1even  15513  oddnn02np1  15518  oddge22np1  15519  evennn02n  15520  evennn2n  15521  divalglem4  15568  divalgb  15576  modremain  15580  modprmn0modprm0  15961  vdwlem6  16139  vdwlem11  16144  vdw  16147  ramval  16161  imasleval  16631  dfiso3  16860  fullestrcsetc  17218  fullsetcestrc  17233  isipodrs  17588  ipodrsfi  17590  gsumpropd2lem  17700  mndpropd  17743  grppropd  17864  conjnmzb  18122  symgextfo  18269  symgfixfo  18286  sylow1lem2  18442  sylow3lem1  18470  sylow3lem3  18472  lsmelvalm  18494  lsmass  18511  iscyg3  18716  ghmcyg  18725  cycsubgcyg  18730  pgpfac1lem2  18902  pgpfac1lem4  18905  ablfac2  18916  dvdsr02  19084  crngunit  19090  dvdsrpropd  19124  lpigen  19706  znunit  20380  elfilspd  20617  scmatmats  20792  symgmatr01  20935  isclo  21367  iscnp3  21524  lmbrf  21540  cncnp  21560  lmss  21578  isnrm2  21638  cmpfi  21688  1stcfb  21725  1stccnp  21742  ptrescn  21919  txkgen  21932  xkoinjcn  21967  trfil3  22168  fmid  22240  lmflf  22285  txflf  22286  ptcmplem3  22334  tsmsf1o  22424  ucnprima  22562  metrest  22805  metcnp  22822  metcnp2  22823  txmetcnp  22828  metuel2  22846  metustbl  22847  psmetutop  22848  metucn  22852  evth2  23235  lmmbrf  23536  iscfil2  23540  fmcfil  23546  iscau2  23551  iscau4  23553  iscauf  23554  caucfil  23557  iscmet3lem3  23564  cfilresi  23569  causs  23572  lmclim  23577  ivth2  23727  ovolfioo  23739  ovolficc  23740  ovolshftlem1  23781  ovolscalem1  23785  volsup2  23877  ismbf3d  23926  mbfaddlem  23932  mbfsup  23936  mbfinf  23937  itg2seq  24014  itg2gt0  24032  ellimc2  24146  ellimc3  24148  rolle  24258  cmvth  24259  mvth  24260  dvlip  24261  dvivth  24278  lhop1lem  24281  deg1ldg  24357  ulm2  24644  ulmdvlem3  24661  dcubic  25093  mcubic  25094  cubic2  25095  rlimcnp  25213  ftalem3  25322  isppw2  25362  lgsquadlem2  25627  2lgslem1a  25637  dchrmusumlema  25739  dchrisum0lema  25760  tglowdim2l  26106  mirreu3  26110  oppcom  26200  iscgra1  26266  axsegcon  26384  axpasch  26398  axcontlem7  26427  usgr2pth0  27221  usgr2wspthon  27419  elwwlks2  27420  elwspths2spth  27421  rusgrnumwwlks  27428  clwwlkfo  27504  eclclwwlkn1  27529  eucrctshift  27698  fusgreg2wsp  27795  nmobndi  28231  nmounbi  28232  nmoo0  28247  h2hcau  28435  h2hlm  28436  shsel3  28771  pjhtheu2  28872  chscllem2  29094  adjbdln  29539  branmfn  29561  pjimai  29632  chrelati  29820  cdj3lem3  29894  cdj3lem3b  29896  dfimafnf  30044  ofpreima  30073  isarchi2  30410  submarchi  30411  archirng  30413  archiabl  30423  isarchiofld  30499  ellspds  30536  fedgmullem2  30585  ordtconnlem1  30740  lmdvg  30769  esumfsup  30902  dya2icoseg2  31109  eulerpartlemgh  31209  ballotlemodife  31328  ballotlemsima  31346  erdszelem10  32011  iscvm  32070  wsuclem  32666  etasslt  32828  seglelin  33131  outsideofeu  33146  opnrebl  33222  opnrebl2  33223  filnetlem4  33283  bj-finsumval0  34065  phpreu  34353  ptrest  34368  poimirlem3  34372  poimirlem4  34373  poimirlem17  34386  poimirlem26  34395  poimirlem27  34396  broucube  34403  mblfinlem1  34406  lmclim2  34511  caures  34513  isbnd3b  34541  heiborlem7  34573  heiborlem10  34576  rrncmslem  34588  isdrngo2  34714  erim2  35392  prter3  35499  islshpsm  35597  lsatfixedN  35626  lrelat  35631  eqlkr2  35717  lshpkrlem1  35727  lfl1dim  35738  eqlkr4  35782  ishlat3N  35971  hlsupr2  36004  hlrelat5N  36018  hlrelat  36019  cvrval5  36032  cvrat42  36061  athgt  36073  3dim0  36074  islln3  36127  llnexatN  36138  islpln3  36150  islvol3  36193  islvol5  36196  isline4N  36394  polval2N  36523  4atex3  36698  cdleme0ex2N  36841  cdlemefrs29cpre1  37015  cdlemb3  37223  cdlemg33c  37325  cdlemg33e  37327  dia1dim2  37679  cdlemm10N  37735  dib1dim2  37785  diclspsn  37811  dih1dimatlem  37946  dihatexv2  37956  djhcvat42  38032  dihjat1lem  38045  dvh4dimat  38055  dvh2dimatN  38057  lcfrlem9  38167  mapdval4N  38249  mapdcv  38277  elrfirn  38727  elrfirn2  38728  mrefg3  38740  diophin  38805  diophun  38806  diophren  38846  rmxycomplete  38950  wepwsolem  39078  fnwe2lem2  39087  islssfg  39106  ntrneineine0lem  39869  ntrneineine1lem  39870  ntrneiel2  39872  extoimad  39952  grumnudlem  40070  supsubc  41115  infxrbnd2  41131  supminfxr  41236  evthiccabs  41267  elicores  41305  clim2f  41413  clim2cf  41427  clim0cf  41431  clim2f2  41447  limsupub  41481  limsupmnflem  41497  limsupre2lem  41501  limsuplt2  41530  liminfreuzlem  41579  liminfltlem  41581  liminflimsupclim  41584  xlimmnfmpt  41620  xlimpnfmpt  41621  fourierdlem73  41960  fourierdlem83  41970  meaiuninc3v  42262  ovolval2  42422  dfaimafn  42834  iccelpart  43029  sprsymrelf  43093  sprsymrelfo  43095  fmtnoprmfac1  43163  fmtnoprmfac2  43165  fmtnofac2lem  43166  dfeven2  43250  dfodd3  43251  isomuspgrlem2d  43432  uspgrsprfo  43459  elbigo2  44047  rrxlinesc  44157  rrxlinec  44158  rrx2line  44162  rrx2vlinest  44163  itsclquadeu  44199