Theorem exbidv 1825

Description: Formula-building rule for existential quantifier (deduction form). (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
albidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
exbidv	⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem exbidv

Step	Hyp	Ref	Expression
1		ax-17 1526	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		albidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	exbidh 1614	1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 105  ∃wex 1492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11ev  1828  2exbidv  1868  3exbidv  1869  eubidh  2032  eubid  2033  eleq1w  2238  eleq2w  2239  eleq1  2240  eleq2  2241  rexbidv2  2480  ceqsex2  2778  alexeq  2864  ceqex  2865  sbc5  2987  sbcex2  3017  sbcexg  3018  sbcabel  3045  eluni  3813  csbunig  3818  intab  3874  cbvopab1  4077  cbvopab1s  4079  axsep2  4123  zfauscl  4124  bnd2  4174  mss  4227  opeqex  4250  euotd  4255  snnex  4449  uniuni  4452  regexmid  4535  reg2exmid  4536  onintexmid  4573  reg3exmid  4580  nnregexmid  4621  opeliunxp  4682  csbxpg  4708  brcog  4795  elrn2g  4818  dfdmf  4821  csbdmg  4822  eldmg  4823  dfrnf  4869  elrn2  4870  elrnmpt1  4879  brcodir  5017  xp11m  5068  xpimasn  5078  csbrng  5091  elxp4  5117  elxp5  5118  dfco2a  5130  cores  5133  funimaexglem  5300  brprcneu  5509  ssimaexg  5579  dmfco  5585  fndmdif  5622  fmptco  5683  fliftf  5800  acexmidlem2  5872  acexmidlemv  5873  cbvoprab1  5947  cbvoprab2  5948  oprssdmm  6172  dmtpos  6257  tfrlemi1  6333  tfr1onlemaccex  6349  tfrcllemaccex  6362  ecdmn0m  6577  ereldm  6578  elqsn0m  6603  mapsn  6690  bren  6747  brdomg  6748  domeng  6752  ac6sfi  6898  ordiso  7035  ctssdclemr  7111  enumct  7114  ctssexmid  7148  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  acfun  7206  ccfunen  7263  cc1  7264  cc2lem  7265  cc2  7266  cc3  7267  recexnq  7389  prarloc  7502  genpdflem  7506  genpassl  7523  genpassu  7524  ltexprlemell  7597  ltexprlemelu  7598  ltexprlemm  7599  recexprlemell  7621  recexprlemelu  7622  cnm  7831  sup3exmid  8914  seq3f1olemp  10502  zfz1isolem1  10820  zfz1iso  10821  sumeq1  11363  sumeq2  11367  summodc  11391  fsum3  11395  fsum2dlemstep  11442  ntrivcvgap0  11557  prodeq1f  11560  prodeq2w  11564  prodeq2  11565  prodmodc  11586  zproddc  11587  fprodseq  11591  fprodntrivap  11592  fprod2dlemstep  11630  ctinf  12431  ctiunct  12441  ssomct  12446  ptex  12713  bdsep2  14641  bdzfauscl  14645  strcoll2  14738  sscoll2  14743  subctctexmid  14753  nninfall  14761