Theorem rexbidva 3162

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

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

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 3061

This theorem is referenced by:  rexbidv  3164  2rexbiia  3202  2rexbidva  3204  rexeqbidva  3312  frinxp  5737  onfr  6391  dfimafn  6940  funimass4  6942  fliftel  7301  fliftf  7307  isomin  7329  f1oiso  7343  releldm2  8040  oaass  8571  eldifsucnn  8674  cofonr  8684  naddunif  8703  qsinxp  8805  qliftel  8812  fimaxg  9293  ordunifi  9296  supisolem  9484  fiming  9510  wemapwe  9709  ttrcltr  9728  ttrclse  9739  frmin  9761  cflim2  10275  cfsmolem  10282  alephsing  10288  brdom7disj  10543  brdom6disj  10544  alephreg  10594  nqereu  10941  1idpr  11041  map2psrpr  11122  axsup  11308  rereccl  11957  sup3  12197  infm3  12199  supadd  12208  creur  12232  creui  12233  nndiv  12284  nnrecl  12497  rpnnen1lem2  12991  rpnnen1lem1  12992  rpnnen1lem3  12993  rpnnen1lem5  12995  supxrbnd1  13335  supxrbnd2  13336  supxrbnd  13342  rabssnn0fi  14002  mptnn0fsupp  14013  expnlbnd  14249  wrdl3s3  14979  limsuplt  15493  clim2  15518  clim2c  15519  clim0c  15521  ello12  15530  elo12  15541  rlimresb  15579  climabs0  15599  sumeq2ii  15707  mertens  15900  prodeq2ii  15925  zprod  15951  nndivides  16280  alzdvds  16337  oddm1even  16360  oddnn02np1  16365  oddge22np1  16366  evennn02n  16367  evennn2n  16368  divalglem4  16413  divalgb  16421  modremain  16425  modprmn0modprm0  16825  vdwlem6  17004  vdwlem11  17009  vdw  17012  ramval  17026  imasleval  17553  dfiso3  17784  fullestrcsetc  18161  fullsetcestrc  18176  isipodrs  18545  ipodrsfi  18547  gsumpropd2lem  18655  mndpropd  18735  grppropd  18932  qus0subgbas  19179  conjnmzb  19234  symgextfo  19401  symgfixfo  19418  sylow1lem2  19578  sylow3lem1  19606  sylow3lem3  19608  lsmelvalm  19630  lsmass  19648  iscyg3  19865  ghmcyg  19875  cycsubgcyg  19880  pgpfac1lem2  20056  pgpfac1lem4  20059  ablfac2  20070  dvdsr02  20330  crngunit  20336  dvdsrpropd  20374  rngqiprngimfo  21260  lpigen  21294  pzriprnglem10  21449  znunit  21522  elfilspd  21761  psdmul  22102  scmatmats  22447  symgmatr01  22590  isclo  23023  iscnp3  23180  lmbrf  23196  cncnp  23216  lmss  23234  isnrm2  23294  cmpfi  23344  1stcfb  23381  1stccnp  23398  ptrescn  23575  txkgen  23588  xkoinjcn  23623  trfil3  23824  fmid  23896  lmflf  23941  txflf  23942  ptcmplem3  23990  tsmsf1o  24081  ucnprima  24218  metrest  24461  metcnp  24478  metcnp2  24479  txmetcnp  24484  metuel2  24502  metustbl  24503  psmetutop  24504  metucn  24508  evth2  24908  lmmbrf  25212  iscfil2  25216  fmcfil  25222  iscau2  25227  iscau4  25229  iscauf  25230  caucfil  25233  iscmet3lem3  25240  cfilresi  25245  causs  25248  lmclim  25253  ivth2  25406  ovolfioo  25418  ovolficc  25419  ovolshftlem1  25460  ovolscalem1  25464  volsup2  25556  ismbf3d  25605  mbfaddlem  25611  mbfsup  25615  mbfinf  25616  itg2seq  25693  itg2gt0  25711  ellimc2  25828  ellimc3  25830  rolle  25944  cmvth  25945  cmvthOLD  25946  mvth  25947  dvlip  25948  dvivth  25965  lhop1lem  25968  deg1ldg  26047  ulm2  26344  ulmdvlem3  26361  dcubic  26806  mcubic  26807  cubic2  26808  rlimcnp  26925  ftalem3  27035  isppw2  27075  lgsquadlem2  27342  2lgslem1a  27352  dchrmusumlema  27454  dchrisum0lema  27475  cofcutr  27875  lrrecfr  27893  addsrid  27914  addscom  27916  addsuniflem  27951  addsass  27955  addsbday  27967  negsunif  28004  mulsrid  28056  mulsasslem3  28108  n0s0suc  28262  renegscl  28347  readdscl  28348  remulscllem2  28350  remulscl  28351  tglowdim2l  28575  mirreu3  28579  oppcom  28669  iscgra1  28735  axsegcon  28852  axpasch  28866  axcontlem7  28895  usgr2pth0  29693  usgr2wspthon  29893  elwwlks2  29894  elwspths2spth  29895  rusgrnumwwlks  29902  clwwlkfo  29977  eclclwwlkn1  30002  eucrctshift  30170  fusgreg2wsp  30263  nmobndi  30702  nmounbi  30703  nmoo0  30718  h2hcau  30906  h2hlm  30907  shsel3  31242  pjhtheu2  31343  chscllem2  31565  adjbdln  32010  branmfn  32032  pjimai  32103  chrelati  32291  cdj3lem3  32365  cdj3lem3b  32367  dfimafnf  32560  ofpreima  32589  isarchi2  33129  submarchi  33130  archirng  33132  archiabl  33142  isarchiofld  33285  ellspds  33329  dvdsruasso2  33347  lsmssass  33363  grplsm0l  33364  fedgmullem2  33616  elirng  33673  zarcls  33851  ordtconnlem1  33901  lmdvg  33930  esumfsup  34047  dya2icoseg2  34256  eulerpartlemgh  34356  ballotlemodife  34476  ballotlemsima  34494  nummin  35068  erdszelem10  35168  iscvm  35227  wsuclem  35789  seglelin  36080  outsideofeu  36095  opnrebl  36284  opnrebl2  36285  filnetlem4  36345  bj-finsumval0  37249  phpreu  37574  ptrest  37589  poimirlem3  37593  poimirlem4  37594  poimirlem17  37607  poimirlem26  37616  poimirlem27  37617  broucube  37624  mblfinlem1  37627  lmclim2  37728  caures  37730  isbnd3b  37755  heiborlem7  37787  heiborlem10  37790  rrncmslem  37802  isdrngo2  37928  erimeq2  38642  prter3  38846  islshpsm  38944  lsatfixedN  38973  lrelat  38978  eqlkr2  39064  lshpkrlem1  39074  lfl1dim  39085  eqlkr4  39129  ishlat3N  39318  hlsupr2  39352  hlrelat5N  39366  hlrelat  39367  cvrval5  39380  cvrat42  39409  athgt  39421  3dim0  39422  islln3  39475  llnexatN  39486  islpln3  39498  islvol3  39541  islvol5  39544  isline4N  39742  polval2N  39871  4atex3  40046  cdleme0ex2N  40189  cdlemefrs29cpre1  40363  cdlemb3  40571  cdlemg33c  40673  cdlemg33e  40675  dia1dim2  41027  cdlemm10N  41083  dib1dim2  41133  diclspsn  41159  dih1dimatlem  41294  dihatexv2  41304  djhcvat42  41380  dihjat1lem  41393  dvh4dimat  41403  dvh2dimatN  41405  lcfrlem9  41515  mapdval4N  41597  mapdcv  41625  ef11d  42335  cxp112d  42337  cxp111d  42338  sn-sup3d  42462  fimgmcyc  42504  infdesc  42613  elrfirn  42665  elrfirn2  42666  mrefg3  42678  diophin  42742  diophun  42743  diophren  42783  rmxycomplete  42888  wepwsolem  43013  fnwe2lem2  43022  islssfg  43041  unielss  43189  onmaxnelsup  43194  onsupnmax  43199  onsupeqnmax  43218  tfsconcat0i  43316  ntrneineine0lem  44054  ntrneineine1lem  44055  ntrneiel2  44057  extoimad  44135  grumnudlem  44257  modelac8prim  44965  supsubc  45328  infxrbnd2  45344  supminfxr  45439  evthiccabs  45473  elicores  45510  clim2f  45613  clim2cf  45627  clim0cf  45631  clim2f2  45647  limsupub  45681  limsupmnflem  45697  limsupre2lem  45701  limsuplt2  45730  liminfreuzlem  45779  liminfltlem  45781  liminflimsupclim  45784  xlimmnfmpt  45820  xlimpnfmpt  45821  fourierdlem73  46156  fourierdlem83  46166  meaiuninc3v  46461  ovolval2  46621  cfsetsnfsetfo  47037  dfaimafn  47142  iccelpart  47395  sprsymrelf  47457  sprsymrelfo  47459  fmtnoprmfac1  47527  fmtnoprmfac2  47529  fmtnofac2lem  47530  dfeven2  47611  dfodd3  47612  dfvopnbgr2  47814  usgrgrtrirex  47910  stgredgiun  47918  uspgrsprfo  48071  elbigo2  48480  rrxlinesc  48663  rrxlinec  48664  rrx2line  48668  rrx2vlinest  48669  itsclquadeu  48705