Theorem rexbidva 3184

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ∈ wcel 2142  ∃wrex 3086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-rex 3087

This theorem is referenced by:  rexbidv  3186  2rexbiia  3223  2rexbidva  3225  rexeqbidva  3327  frinxp  5730  onfr  6385  dfimafn  6929  funimass4  6931  fliftel  7293  fliftf  7299  isomin  7321  f1oiso  7335  releldm2  8024  oaass  8530  eldifsucnn  8634  cofonr  8644  naddunif  8664  qsinxp  8775  qliftel  8782  fimaxg  9231  ordunifi  9234  supisolem  9420  fiming  9446  wemapwe  9652  ttrcltr  9671  ttrclse  9682  frmin  9707  cflim2  10220  cfsmolem  10227  alephsing  10233  brdom7disj  10488  brdom6disj  10489  alephreg  10540  nqereu  10887  1idpr  10987  map2psrpr  11068  axsup  11258  rereccl  11909  sup3  12149  infm3  12151  supadd  12160  creur  12189  creui  12190  nndiv  12259  nnrecl  12479  rpnnen1lem2  12978  rpnnen1lem1  12979  rpnnen1lem3  12980  rpnnen1lem5  12982  supxrbnd1  13324  supxrbnd2  13325  supxrbnd  13331  rabssnn0fi  13999  mptnn0fsupp  14010  expnlbnd  14246  wrdl3s3  14975  limsuplt  15506  clim2  15531  clim2c  15532  clim0c  15534  ello12  15543  elo12  15554  rlimresb  15592  climabs0  15612  sumeq2ii  15720  mertens  15916  prodeq2ii  15941  zprod  15967  nndivides  16296  alzdvds  16354  oddm1even  16377  oddnn02np1  16382  oddge22np1  16383  evennn02n  16384  evennn2n  16385  divalglem4  16430  divalgb  16438  modremain  16442  modprmn0modprm0  16843  vdwlem6  17022  vdwlem11  17027  vdw  17030  ramval  17044  imasleval  17571  dfiso3  17806  fullestrcsetc  18183  fullsetcestrc  18198  isipodrs  18569  ipodrsfi  18571  gsumpropd2lem  18713  mndpropd  18793  grppropd  18993  qus0subgbas  19239  conjnmzb  19293  symgextfo  19462  symgfixfo  19479  sylow1lem2  19639  sylow3lem1  19667  sylow3lem3  19669  lsmelvalm  19691  lsmass  19709  iscyg3  19926  ghmcyg  19936  cycsubgcyg  19941  pgpfac1lem2  20117  pgpfac1lem4  20120  ablfac2  20131  dvdsr02  20417  crngunit  20423  dvdsrpropd  20461  rngqiprngimfo  21368  lpigen  21402  pzriprnglem10  21539  znunit  21612  elfilspd  21852  psdmul  22228  scmatmats  22568  symgmatr01  22711  isclo  23144  iscnp3  23301  lmbrf  23317  cncnp  23337  lmss  23355  isnrm2  23415  cmpfi  23465  1stcfb  23502  1stccnp  23519  ptrescn  23696  txkgen  23709  xkoinjcn  23744  trfil3  23945  fmid  24017  lmflf  24062  txflf  24063  ptcmplem3  24111  tsmsf1o  24202  ucnprima  24338  metrest  24581  metcnp  24598  metcnp2  24599  txmetcnp  24604  metuel2  24622  metustbl  24623  psmetutop  24624  metucn  24628  evth2  25019  lmmbrf  25321  iscfil2  25325  fmcfil  25331  iscau2  25336  iscau4  25338  iscauf  25339  caucfil  25342  iscmet3lem3  25349  cfilresi  25354  causs  25357  lmclim  25362  ivth2  25514  ovolfioo  25526  ovolficc  25527  ovolshftlem1  25568  ovolscalem1  25572  volsup2  25664  ismbf3d  25713  mbfaddlem  25719  mbfsup  25723  mbfinf  25724  itg2seq  25801  itg2gt0  25819  ellimc2  25936  ellimc3  25938  rolle  26049  cmvth  26050  mvth  26051  dvlip  26052  dvivth  26069  lhop1lem  26072  deg1ldg  26149  ulm2  26445  ulmdvlem3  26462  dcubic  26908  mcubic  26909  cubic2  26910  rlimcnp  27027  ftalem3  27136  isppw2  27176  lgsquadlem2  27442  2lgslem1a  27452  dchrmusumlema  27554  dchrisum0lema  27575  cofcutr  28014  lrrecfr  28033  addsrid  28054  addscom  28056  addsuniflem  28091  addsass  28095  addbday  28108  negsunif  28145  mulsrid  28203  mulsasslem3  28255  n0s0suc  28432  z12sge0  28573  elreno2  28585  renegscl  28588  readdscl  28589  remulscllem2  28591  remulscl  28592  tglowdim2l  28817  mirreu3  28824  oppcom  28914  iscgra1  29001  axsegcon  29125  axpasch  29139  axcontlem7  29168  usgr2pth0  29962  usgr2wspthon  30165  elwwlks2  30166  elwspths2spth  30167  rusgrnumwwlks  30174  clwwlkfo  30249  eclclwwlkn1  30274  eucrctshift  30442  fusgreg2wsp  30535  nmobndi  30975  nmounbi  30976  nmoo0  30991  h2hcau  31179  h2hlm  31180  shsel3  31515  pjhtheu2  31616  chscllem2  31838  adjbdln  32283  branmfn  32305  pjimai  32376  chrelati  32564  cdj3lem3  32638  cdj3lem3b  32640  dfimafnf  32835  ofpreima  32864  isarchi2  33362  submarchi  33363  archirng  33365  archiabl  33375  isarchiofld  33376  isunitc  33419  ellspds  33551  dvdsruasso2  33569  lsmssass  33585  grplsm0l  33586  fedgmullem2  33924  elirng  33980  zarcls  34168  ordtconnlem1  34218  lmdvg  34247  esumfsup  34364  dya2icoseg2  34572  eulerpartlemgh  34672  ballotlemodife  34792  ballotlemsima  34810  nummin  35386  erdszelem10  35547  iscvm  35606  wsuclem  36170  seglelin  36463  outsideofeu  36478  opnrebl  36677  opnrebl2  36678  filnetlem4  36738  bj-finsumval0  37774  phpreu  38100  ptrest  38115  poimirlem3  38119  poimirlem4  38120  poimirlem17  38133  poimirlem26  38142  poimirlem27  38143  broucube  38150  mblfinlem1  38153  lmclim2  38254  caures  38256  isbnd3b  38281  heiborlem7  38313  heiborlem10  38316  rrncmslem  38328  isdrngo2  38454  erimeq2  39259  prter3  39503  islshpsm  39601  lsatfixedN  39630  lrelat  39635  eqlkr2  39721  lshpkrlem1  39731  lfl1dim  39742  eqlkr4  39786  ishlat3N  39975  hlsupr2  40008  hlrelat5N  40022  hlrelat  40023  cvrval5  40036  cvrat42  40065  athgt  40077  3dim0  40078  islln3  40131  llnexatN  40142  islpln3  40154  islvol3  40197  islvol5  40200  isline4N  40398  polval2N  40527  4atex3  40702  cdleme0ex2N  40845  cdlemefrs29cpre1  41019  cdlemb3  41227  cdlemg33c  41329  cdlemg33e  41331  dia1dim2  41683  cdlemm10N  41739  dib1dim2  41789  diclspsn  41815  dih1dimatlem  41950  dihatexv2  41960  djhcvat42  42036  dihjat1lem  42049  dvh4dimat  42059  dvh2dimatN  42061  lcfrlem9  42171  mapdval4N  42253  mapdcv  42281  ef11d  42945  cxp112d  42947  cxp111d  42948  sn-sup3d  43111  fimgmcyc  43149  infdesc  43222  elrfirn  43273  elrfirn2  43274  mrefg3  43286  diophin  43350  diophun  43351  diophren  43387  rmxycomplete  43491  wepwsolem  43616  fnwe2lem2  43625  islssfg  43644  unielss  43792  onmaxnelsup  43797  onsupnmax  43802  onsupeqnmax  43821  tfsconcat0i  43919  ntrneineine0lem  44656  ntrneineine1lem  44657  ntrneiel2  44659  extoimad  44737  grumnudlem  44858  modelac8prim  45565  supsubc  45926  infxrbnd2  45941  supminfxr  46035  evthiccabs  46069  elicores  46106  clim2f  46207  clim2cf  46221  clim0cf  46225  clim2f2  46241  limsupub  46275  limsupmnflem  46291  limsupre2lem  46295  limsuplt2  46324  liminfreuzlem  46373  liminfltlem  46375  liminflimsupclim  46378  xlimmnfmpt  46414  xlimpnfmpt  46415  fourierdlem73  46750  fourierdlem83  46760  meaiuninc3v  47055  ovolval2  47215  cfsetsnfsetfo  47651  dfaimafn  47756  iccelpart  48036  sprsymrelf  48098  sprsymrelfo  48100  nprmmul1  48130  nprmmul3  48132  fmtnoprmfac1  48171  fmtnoprmfac2  48173  fmtnofac2lem  48174  dfeven2  48268  dfodd3  48269  dfvopnbgr2  48472  usgrgrtrirex  48569  stgredgiun  48577  uspgrsprfo  48767  elbigo2  49171  rrxlinesc  49354  rrxlinec  49355  rrx2line  49359  rrx2vlinest  49360  itsclquadeu  49396