Theorem rexbidva 3175

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∈ wcel 2105  ∃wrex 3069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-rex 3070

This theorem is referenced by:  rexbidv  3177  2rexbiia  3214  2rexbidva  3216  rexeqbidva  3327  frinxp  5758  onfr  6403  dfimafn  6954  funimass4  6956  fliftel  7309  fliftf  7315  isomin  7337  f1oiso  7351  releldm2  8032  oaass  8564  eldifsucnn  8666  cofonr  8676  naddunif  8695  qsinxp  8790  qliftel  8797  fimaxg  9293  ordunifi  9296  supisolem  9471  fiming  9496  wemapwe  9695  ttrcltr  9714  ttrclse  9725  frmin  9747  cflim2  10261  cfsmolem  10268  alephsing  10274  brdom7disj  10529  brdom6disj  10530  alephreg  10580  nqereu  10927  1idpr  11027  map2psrpr  11108  axsup  11294  rereccl  11937  sup3  12176  infm3  12178  supadd  12187  creur  12211  creui  12212  nndiv  12263  nnrecl  12475  rpnnen1lem2  12966  rpnnen1lem1  12967  rpnnen1lem3  12968  rpnnen1lem5  12970  supxrbnd1  13305  supxrbnd2  13306  supxrbnd  13312  rabssnn0fi  13956  mptnn0fsupp  13967  expnlbnd  14201  wrdl3s3  14918  limsuplt  15428  clim2  15453  clim2c  15454  clim0c  15456  ello12  15465  elo12  15476  rlimresb  15514  climabs0  15534  sumeq2ii  15644  mertens  15837  prodeq2ii  15862  zprod  15886  nndivides  16212  alzdvds  16268  oddm1even  16291  oddnn02np1  16296  oddge22np1  16297  evennn02n  16298  evennn2n  16299  divalglem4  16344  divalgb  16352  modremain  16356  modprmn0modprm0  16745  vdwlem6  16924  vdwlem11  16929  vdw  16932  ramval  16946  imasleval  17492  dfiso3  17725  fullestrcsetc  18108  fullsetcestrc  18123  isipodrs  18495  ipodrsfi  18497  gsumpropd2lem  18605  mndpropd  18685  grppropd  18874  qus0subgbas  19114  conjnmzb  19168  symgextfo  19332  symgfixfo  19349  sylow1lem2  19509  sylow3lem1  19537  sylow3lem3  19539  lsmelvalm  19561  lsmass  19579  iscyg3  19796  ghmcyg  19806  cycsubgcyg  19811  pgpfac1lem2  19987  pgpfac1lem4  19990  ablfac2  20001  dvdsr02  20264  crngunit  20270  dvdsrpropd  20308  rngqiprngimfo  21061  lpigen  21095  pzriprnglem10  21260  znunit  21339  elfilspd  21578  scmatmats  22234  symgmatr01  22377  isclo  22812  iscnp3  22969  lmbrf  22985  cncnp  23005  lmss  23023  isnrm2  23083  cmpfi  23133  1stcfb  23170  1stccnp  23187  ptrescn  23364  txkgen  23377  xkoinjcn  23412  trfil3  23613  fmid  23685  lmflf  23730  txflf  23731  ptcmplem3  23779  tsmsf1o  23870  ucnprima  24008  metrest  24254  metcnp  24271  metcnp2  24272  txmetcnp  24277  metuel2  24295  metustbl  24296  psmetutop  24297  metucn  24301  evth2  24707  lmmbrf  25011  iscfil2  25015  fmcfil  25021  iscau2  25026  iscau4  25028  iscauf  25029  caucfil  25032  iscmet3lem3  25039  cfilresi  25044  causs  25047  lmclim  25052  ivth2  25205  ovolfioo  25217  ovolficc  25218  ovolshftlem1  25259  ovolscalem1  25263  volsup2  25355  ismbf3d  25404  mbfaddlem  25410  mbfsup  25414  mbfinf  25415  itg2seq  25493  itg2gt0  25511  ellimc2  25627  ellimc3  25629  rolle  25743  cmvth  25744  mvth  25745  dvlip  25746  dvivth  25763  lhop1lem  25766  deg1ldg  25846  ulm2  26134  ulmdvlem3  26151  dcubic  26588  mcubic  26589  cubic2  26590  rlimcnp  26707  ftalem3  26816  isppw2  26856  lgsquadlem2  27121  2lgslem1a  27131  dchrmusumlema  27233  dchrisum0lema  27254  cofcutr  27650  lrrecfr  27666  addsrid  27687  addscom  27689  addsuniflem  27724  addsass  27728  negsunif  27769  mulsrid  27809  mulsasslem3  27860  tglowdim2l  28169  mirreu3  28173  oppcom  28263  iscgra1  28329  axsegcon  28453  axpasch  28467  axcontlem7  28496  usgr2pth0  29290  usgr2wspthon  29487  elwwlks2  29488  elwspths2spth  29489  rusgrnumwwlks  29496  clwwlkfo  29571  eclclwwlkn1  29596  eucrctshift  29764  fusgreg2wsp  29857  nmobndi  30296  nmounbi  30297  nmoo0  30312  h2hcau  30500  h2hlm  30501  shsel3  30836  pjhtheu2  30937  chscllem2  31159  adjbdln  31604  branmfn  31626  pjimai  31697  chrelati  31885  cdj3lem3  31959  cdj3lem3b  31961  dfimafnf  32128  ofpreima  32158  isarchi2  32602  submarchi  32603  archirng  32605  archiabl  32615  isarchiofld  32706  ellspds  32756  lsmssass  32787  grplsm0l  32788  fedgmullem2  33004  elirng  33040  zarcls  33153  ordtconnlem1  33203  lmdvg  33232  esumfsup  33367  dya2icoseg2  33576  eulerpartlemgh  33676  ballotlemodife  33795  ballotlemsima  33813  nummin  34393  erdszelem10  34490  iscvm  34549  wsuclem  35102  seglelin  35393  outsideofeu  35408  gg-cmvth  35467  opnrebl  35509  opnrebl2  35510  filnetlem4  35570  bj-finsumval0  36470  phpreu  36776  ptrest  36791  poimirlem3  36795  poimirlem4  36796  poimirlem17  36809  poimirlem26  36818  poimirlem27  36819  broucube  36826  mblfinlem1  36829  lmclim2  36930  caures  36932  isbnd3b  36957  heiborlem7  36989  heiborlem10  36992  rrncmslem  37004  isdrngo2  37130  erimeq2  37852  prter3  38056  islshpsm  38154  lsatfixedN  38183  lrelat  38188  eqlkr2  38274  lshpkrlem1  38284  lfl1dim  38295  eqlkr4  38339  ishlat3N  38528  hlsupr2  38562  hlrelat5N  38576  hlrelat  38577  cvrval5  38590  cvrat42  38619  athgt  38631  3dim0  38632  islln3  38685  llnexatN  38696  islpln3  38708  islvol3  38751  islvol5  38754  isline4N  38952  polval2N  39081  4atex3  39256  cdleme0ex2N  39399  cdlemefrs29cpre1  39573  cdlemb3  39781  cdlemg33c  39883  cdlemg33e  39885  dia1dim2  40237  cdlemm10N  40293  dib1dim2  40343  diclspsn  40369  dih1dimatlem  40504  dihatexv2  40514  djhcvat42  40590  dihjat1lem  40603  dvh4dimat  40613  dvh2dimatN  40615  lcfrlem9  40725  mapdval4N  40807  mapdcv  40835  infdesc  41688  elrfirn  41736  elrfirn2  41737  mrefg3  41749  diophin  41813  diophun  41814  diophren  41854  rmxycomplete  41959  wepwsolem  42087  fnwe2lem2  42096  islssfg  42115  unielss  42270  onmaxnelsup  42275  onsupnmax  42280  onsupeqnmax  42299  tfsconcat0i  42398  ntrneineine0lem  43137  ntrneineine1lem  43138  ntrneiel2  43140  extoimad  43219  grumnudlem  43347  supsubc  44362  infxrbnd2  44378  supminfxr  44473  evthiccabs  44508  elicores  44545  clim2f  44651  clim2cf  44665  clim0cf  44669  clim2f2  44685  limsupub  44719  limsupmnflem  44735  limsupre2lem  44739  limsuplt2  44768  liminfreuzlem  44817  liminfltlem  44819  liminflimsupclim  44822  xlimmnfmpt  44858  xlimpnfmpt  44859  fourierdlem73  45194  fourierdlem83  45204  meaiuninc3v  45499  ovolval2  45659  cfsetsnfsetfo  46069  dfaimafn  46172  iccelpart  46400  sprsymrelf  46462  sprsymrelfo  46464  fmtnoprmfac1  46532  fmtnoprmfac2  46534  fmtnofac2lem  46535  dfeven2  46616  dfodd3  46617  isomuspgrlem2d  46798  uspgrsprfo  46825  elbigo2  47326  rrxlinesc  47509  rrxlinec  47510  rrx2line  47514  rrx2vlinest  47515  itsclquadeu  47551