Theorem rexbidva 3224

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 578	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒)))
3	2	rexbidv2 3223	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∈ wcel 2108  ∃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:  rexbidv  3225  2rexbiia  3226  2rexbidva  3227  rexeqbidva  3346  frinxp  5660  onfr  6290  dfimafn  6814  funimass4  6816  fliftel  7160  fliftf  7166  isomin  7188  f1oiso  7202  releldm2  7857  oaass  8354  qsinxp  8540  qliftel  8547  fimaxg  8991  ordunifi  8994  supisolem  9162  fiming  9187  wemapwe  9385  cflim2  9950  cfsmolem  9957  alephsing  9963  brdom7disj  10218  brdom6disj  10219  alephreg  10269  nqereu  10616  1idpr  10716  map2psrpr  10797  axsup  10981  rereccl  11623  sup3  11862  infm3  11864  supadd  11873  creur  11897  creui  11898  nndiv  11949  nnrecl  12161  rpnnen1lem2  12646  rpnnen1lem1  12647  rpnnen1lem3  12648  rpnnen1lem5  12650  supxrbnd1  12984  supxrbnd2  12985  supxrbnd  12991  rabssnn0fi  13634  mptnn0fsupp  13645  expnlbnd  13876  wrdl3s3  14605  limsuplt  15116  clim2  15141  clim2c  15142  clim0c  15144  ello12  15153  elo12  15164  rlimresb  15202  climabs0  15222  sumeq2ii  15333  mertens  15526  prodeq2ii  15551  zprod  15575  nndivides  15901  alzdvds  15957  oddm1even  15980  oddnn02np1  15985  oddge22np1  15986  evennn02n  15987  evennn2n  15988  divalglem4  16033  divalgb  16041  modremain  16045  modprmn0modprm0  16436  vdwlem6  16615  vdwlem11  16620  vdw  16623  ramval  16637  imasleval  17169  dfiso3  17402  fullestrcsetc  17784  fullsetcestrc  17799  isipodrs  18170  ipodrsfi  18172  gsumpropd2lem  18278  mndpropd  18325  grppropd  18509  conjnmzb  18784  symgextfo  18945  symgfixfo  18962  sylow1lem2  19119  sylow3lem1  19147  sylow3lem3  19149  lsmelvalm  19171  lsmass  19190  iscyg3  19401  ghmcyg  19412  cycsubgcyg  19417  pgpfac1lem2  19593  pgpfac1lem4  19596  ablfac2  19607  dvdsr02  19813  crngunit  19819  dvdsrpropd  19853  lpigen  20440  znunit  20683  elfilspd  20920  scmatmats  21568  symgmatr01  21711  isclo  22146  iscnp3  22303  lmbrf  22319  cncnp  22339  lmss  22357  isnrm2  22417  cmpfi  22467  1stcfb  22504  1stccnp  22521  ptrescn  22698  txkgen  22711  xkoinjcn  22746  trfil3  22947  fmid  23019  lmflf  23064  txflf  23065  ptcmplem3  23113  tsmsf1o  23204  ucnprima  23342  metrest  23586  metcnp  23603  metcnp2  23604  txmetcnp  23609  metuel2  23627  metustbl  23628  psmetutop  23629  metucn  23633  evth2  24029  lmmbrf  24331  iscfil2  24335  fmcfil  24341  iscau2  24346  iscau4  24348  iscauf  24349  caucfil  24352  iscmet3lem3  24359  cfilresi  24364  causs  24367  lmclim  24372  ivth2  24524  ovolfioo  24536  ovolficc  24537  ovolshftlem1  24578  ovolscalem1  24582  volsup2  24674  ismbf3d  24723  mbfaddlem  24729  mbfsup  24733  mbfinf  24734  itg2seq  24812  itg2gt0  24830  ellimc2  24946  ellimc3  24948  rolle  25059  cmvth  25060  mvth  25061  dvlip  25062  dvivth  25079  lhop1lem  25082  deg1ldg  25162  ulm2  25449  ulmdvlem3  25466  dcubic  25901  mcubic  25902  cubic2  25903  rlimcnp  26020  ftalem3  26129  isppw2  26169  lgsquadlem2  26434  2lgslem1a  26444  dchrmusumlema  26546  dchrisum0lema  26567  tglowdim2l  26915  mirreu3  26919  oppcom  27009  iscgra1  27075  axsegcon  27198  axpasch  27212  axcontlem7  27241  usgr2pth0  28034  usgr2wspthon  28231  elwwlks2  28232  elwspths2spth  28233  rusgrnumwwlks  28240  clwwlkfo  28315  eclclwwlkn1  28340  eucrctshift  28508  fusgreg2wsp  28601  nmobndi  29038  nmounbi  29039  nmoo0  29054  h2hcau  29242  h2hlm  29243  shsel3  29578  pjhtheu2  29679  chscllem2  29901  adjbdln  30346  branmfn  30368  pjimai  30439  chrelati  30627  cdj3lem3  30701  cdj3lem3b  30703  dfimafnf  30872  ofpreima  30904  isarchi2  31341  submarchi  31342  archirng  31344  archiabl  31354  isarchiofld  31418  ellspds  31466  lsmssass  31492  grplsm0l  31493  fedgmullem2  31613  zarcls  31726  ordtconnlem1  31776  lmdvg  31805  esumfsup  31938  dya2icoseg2  32145  eulerpartlemgh  32245  ballotlemodife  32364  ballotlemsima  32382  nummin  32963  erdszelem10  33062  iscvm  33121  eldifsucnn  33597  ttrcltr  33702  ttrclse  33713  wsuclem  33746  cofcutr  34019  lrrecfr  34027  addsid1  34054  addscom  34056  seglelin  34345  outsideofeu  34360  opnrebl  34436  opnrebl2  34437  filnetlem4  34497  bj-finsumval0  35383  phpreu  35688  ptrest  35703  poimirlem3  35707  poimirlem4  35708  poimirlem17  35721  poimirlem26  35730  poimirlem27  35731  broucube  35738  mblfinlem1  35741  lmclim2  35843  caures  35845  isbnd3b  35870  heiborlem7  35902  heiborlem10  35905  rrncmslem  35917  isdrngo2  36043  erim2  36716  prter3  36823  islshpsm  36921  lsatfixedN  36950  lrelat  36955  eqlkr2  37041  lshpkrlem1  37051  lfl1dim  37062  eqlkr4  37106  ishlat3N  37295  hlsupr2  37328  hlrelat5N  37342  hlrelat  37343  cvrval5  37356  cvrat42  37385  athgt  37397  3dim0  37398  islln3  37451  llnexatN  37462  islpln3  37474  islvol3  37517  islvol5  37520  isline4N  37718  polval2N  37847  4atex3  38022  cdleme0ex2N  38165  cdlemefrs29cpre1  38339  cdlemb3  38547  cdlemg33c  38649  cdlemg33e  38651  dia1dim2  39003  cdlemm10N  39059  dib1dim2  39109  diclspsn  39135  dih1dimatlem  39270  dihatexv2  39280  djhcvat42  39356  dihjat1lem  39369  dvh4dimat  39379  dvh2dimatN  39381  lcfrlem9  39491  mapdval4N  39573  mapdcv  39601  infdesc  40396  elrfirn  40433  elrfirn2  40434  mrefg3  40446  diophin  40510  diophun  40511  diophren  40551  rmxycomplete  40655  wepwsolem  40783  fnwe2lem2  40792  islssfg  40811  ntrneineine0lem  41582  ntrneineine1lem  41583  ntrneiel2  41585  extoimad  41664  grumnudlem  41792  supsubc  42782  infxrbnd2  42798  supminfxr  42894  evthiccabs  42924  elicores  42961  clim2f  43067  clim2cf  43081  clim0cf  43085  clim2f2  43101  limsupub  43135  limsupmnflem  43151  limsupre2lem  43155  limsuplt2  43184  liminfreuzlem  43233  liminfltlem  43235  liminflimsupclim  43238  xlimmnfmpt  43274  xlimpnfmpt  43275  fourierdlem73  43610  fourierdlem83  43620  meaiuninc3v  43912  ovolval2  44072  cfsetsnfsetfo  44441  dfaimafn  44544  iccelpart  44773  sprsymrelf  44835  sprsymrelfo  44837  fmtnoprmfac1  44905  fmtnoprmfac2  44907  fmtnofac2lem  44908  dfeven2  44989  dfodd3  44990  isomuspgrlem2d  45171  uspgrsprfo  45198  elbigo2  45786  rrxlinesc  45969  rrxlinec  45970  rrx2line  45974  rrx2vlinest  45975  itsclquadeu  46011