Theorem rexbidva 3296

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∈ wcel 2114  ∃wrex 3139

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 1911

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-rex 3144

This theorem is referenced by:  rexbidv  3297  2rexbiia  3298  2rexbidva  3299  rexeqbidva  3426  frinxp  5634  onfr  6230  dfimafn  6728  funimass4  6730  fliftel  7062  fliftf  7068  isomin  7090  f1oiso  7104  releldm2  7742  oaass  8187  qsinxp  8373  qliftel  8380  fimaxg  8765  ordunifi  8768  supisolem  8937  fiming  8962  wemapwe  9160  cflim2  9685  cfsmolem  9692  alephsing  9698  brdom7disj  9953  brdom6disj  9954  alephreg  10004  nqereu  10351  1idpr  10451  map2psrpr  10532  axsup  10716  rereccl  11358  sup3  11598  infm3  11600  supadd  11609  creur  11632  creui  11633  nndiv  11684  nnrecl  11896  rpnnen1lem2  12377  rpnnen1lem1  12378  rpnnen1lem3  12379  rpnnen1lem5  12381  supxrbnd1  12715  supxrbnd2  12716  supxrbnd  12722  rabssnn0fi  13355  mptnn0fsupp  13366  expnlbnd  13595  wrdl3s3  14326  limsuplt  14836  clim2  14861  clim2c  14862  clim0c  14864  ello12  14873  elo12  14884  rlimresb  14922  climabs0  14942  sumeq2ii  15050  mertens  15242  prodeq2ii  15267  zprod  15291  nndivides  15617  alzdvds  15670  oddm1even  15692  oddnn02np1  15697  oddge22np1  15698  evennn02n  15699  evennn2n  15700  divalglem4  15747  divalgb  15755  modremain  15759  modprmn0modprm0  16144  vdwlem6  16322  vdwlem11  16327  vdw  16330  ramval  16344  imasleval  16814  dfiso3  17043  fullestrcsetc  17401  fullsetcestrc  17416  isipodrs  17771  ipodrsfi  17773  gsumpropd2lem  17889  mndpropd  17936  grppropd  18118  conjnmzb  18393  symgextfo  18550  symgfixfo  18567  sylow1lem2  18724  sylow3lem1  18752  sylow3lem3  18754  lsmelvalm  18776  lsmass  18795  iscyg3  19005  ghmcyg  19016  cycsubgcyg  19021  pgpfac1lem2  19197  pgpfac1lem4  19200  ablfac2  19211  dvdsr02  19406  crngunit  19412  dvdsrpropd  19446  lpigen  20029  znunit  20710  elfilspd  20947  scmatmats  21120  symgmatr01  21263  isclo  21695  iscnp3  21852  lmbrf  21868  cncnp  21888  lmss  21906  isnrm2  21966  cmpfi  22016  1stcfb  22053  1stccnp  22070  ptrescn  22247  txkgen  22260  xkoinjcn  22295  trfil3  22496  fmid  22568  lmflf  22613  txflf  22614  ptcmplem3  22662  tsmsf1o  22753  ucnprima  22891  metrest  23134  metcnp  23151  metcnp2  23152  txmetcnp  23157  metuel2  23175  metustbl  23176  psmetutop  23177  metucn  23181  evth2  23564  lmmbrf  23865  iscfil2  23869  fmcfil  23875  iscau2  23880  iscau4  23882  iscauf  23883  caucfil  23886  iscmet3lem3  23893  cfilresi  23898  causs  23901  lmclim  23906  ivth2  24056  ovolfioo  24068  ovolficc  24069  ovolshftlem1  24110  ovolscalem1  24114  volsup2  24206  ismbf3d  24255  mbfaddlem  24261  mbfsup  24265  mbfinf  24266  itg2seq  24343  itg2gt0  24361  ellimc2  24475  ellimc3  24477  rolle  24587  cmvth  24588  mvth  24589  dvlip  24590  dvivth  24607  lhop1lem  24610  deg1ldg  24686  ulm2  24973  ulmdvlem3  24990  dcubic  25424  mcubic  25425  cubic2  25426  rlimcnp  25543  ftalem3  25652  isppw2  25692  lgsquadlem2  25957  2lgslem1a  25967  dchrmusumlema  26069  dchrisum0lema  26090  tglowdim2l  26436  mirreu3  26440  oppcom  26530  iscgra1  26596  axsegcon  26713  axpasch  26727  axcontlem7  26756  usgr2pth0  27546  usgr2wspthon  27744  elwwlks2  27745  elwspths2spth  27746  rusgrnumwwlks  27753  clwwlkfo  27829  eclclwwlkn1  27854  eucrctshift  28022  fusgreg2wsp  28115  nmobndi  28552  nmounbi  28553  nmoo0  28568  h2hcau  28756  h2hlm  28757  shsel3  29092  pjhtheu2  29193  chscllem2  29415  adjbdln  29860  branmfn  29882  pjimai  29953  chrelati  30141  cdj3lem3  30215  cdj3lem3b  30217  dfimafnf  30381  ofpreima  30410  isarchi2  30814  submarchi  30815  archirng  30817  archiabl  30827  isarchiofld  30890  ellspds  30933  fedgmullem2  31026  ordtconnlem1  31167  lmdvg  31196  esumfsup  31329  dya2icoseg2  31536  eulerpartlemgh  31636  ballotlemodife  31755  ballotlemsima  31773  erdszelem10  32447  iscvm  32506  wsuclem  33112  etasslt  33274  seglelin  33577  outsideofeu  33592  opnrebl  33668  opnrebl2  33669  filnetlem4  33729  bj-finsumval0  34570  phpreu  34891  ptrest  34906  poimirlem3  34910  poimirlem4  34911  poimirlem17  34924  poimirlem26  34933  poimirlem27  34934  broucube  34941  mblfinlem1  34944  lmclim2  35048  caures  35050  isbnd3b  35078  heiborlem7  35110  heiborlem10  35113  rrncmslem  35125  isdrngo2  35251  erim2  35926  prter3  36033  islshpsm  36131  lsatfixedN  36160  lrelat  36165  eqlkr2  36251  lshpkrlem1  36261  lfl1dim  36272  eqlkr4  36316  ishlat3N  36505  hlsupr2  36538  hlrelat5N  36552  hlrelat  36553  cvrval5  36566  cvrat42  36595  athgt  36607  3dim0  36608  islln3  36661  llnexatN  36672  islpln3  36684  islvol3  36727  islvol5  36730  isline4N  36928  polval2N  37057  4atex3  37232  cdleme0ex2N  37375  cdlemefrs29cpre1  37549  cdlemb3  37757  cdlemg33c  37859  cdlemg33e  37861  dia1dim2  38213  cdlemm10N  38269  dib1dim2  38319  diclspsn  38345  dih1dimatlem  38480  dihatexv2  38490  djhcvat42  38566  dihjat1lem  38579  dvh4dimat  38589  dvh2dimatN  38591  lcfrlem9  38701  mapdval4N  38783  mapdcv  38811  elrfirn  39312  elrfirn2  39313  mrefg3  39325  diophin  39389  diophun  39390  diophren  39430  rmxycomplete  39534  wepwsolem  39662  fnwe2lem2  39671  islssfg  39690  ntrneineine0lem  40453  ntrneineine1lem  40454  ntrneiel2  40456  extoimad  40535  grumnudlem  40641  supsubc  41641  infxrbnd2  41657  supminfxr  41760  evthiccabs  41791  elicores  41829  clim2f  41937  clim2cf  41951  clim0cf  41955  clim2f2  41971  limsupub  42005  limsupmnflem  42021  limsupre2lem  42025  limsuplt2  42054  liminfreuzlem  42103  liminfltlem  42105  liminflimsupclim  42108  xlimmnfmpt  42144  xlimpnfmpt  42145  fourierdlem73  42484  fourierdlem83  42494  meaiuninc3v  42786  ovolval2  42946  dfaimafn  43384  iccelpart  43613  sprsymrelf  43677  sprsymrelfo  43679  fmtnoprmfac1  43747  fmtnoprmfac2  43749  fmtnofac2lem  43750  dfeven2  43834  dfodd3  43835  isomuspgrlem2d  44016  uspgrsprfo  44043  elbigo2  44632  rrxlinesc  44742  rrxlinec  44743  rrx2line  44747  rrx2vlinest  44748  itsclquadeu  44784