Theorem exbidv 1720

Description: Formula-building rule for existential quantifier (deduction rule). (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 1433	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		albidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	exbidh 1519	1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 102  ∃wex 1395

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1350  ax-gen 1352  ax-ie1 1396  ax-ie2 1397  ax-4 1414  ax-17 1433  ax-ial 1441

This theorem depends on definitions:  df-bi 114

This theorem is referenced by:  ax11ev  1723  2exbidv  1762  3exbidv  1763  eubidh  1920  eubid  1921  eleq1  2114  eleq2  2115  rexbidv2  2344  ceqsex2  2609  alexeq  2690  ceqex  2691  sbc5  2807  sbcex2  2836  sbcexg  2837  sbcabel  2864  eluni  3608  csbunig  3613  intab  3669  cbvopab1  3855  cbvopab1s  3857  axsep2  3901  zfauscl  3902  bnd2  3951  mss  3987  opeqex  4011  euotd  4016  snnex  4206  uniuni  4208  regexmid  4285  reg2exmid  4286  onintexmid  4322  reg3exmid  4329  nnregexmid  4367  opeliunxp  4420  csbxpg  4446  brcog  4527  elrn2g  4550  dfdmf  4553  csbdmg  4554  eldmg  4555  dfrnf  4600  elrn2  4601  elrnmpt1  4610  brcodir  4737  xp11m  4784  xpimasn  4794  csbrng  4807  elxp4  4833  elxp5  4834  dfco2a  4846  cores  4849  funimaexglem  5007  brprcneu  5196  ssimaexg  5260  dmfco  5266  fndmdif  5297  fmptco  5355  fliftf  5464  acexmidlem2  5534  acexmidlemv  5535  cbvoprab1  5601  cbvoprab2  5602  dmtpos  5899  tfrlemi1  5974  ecdmn0m  6176  ereldm  6177  elqsn0m  6202  bren  6256  brdomg  6257  domeng  6261  ac6sfi  6380  ordiso  6386  recexnq  6516  prarloc  6629  genpdflem  6633  genpassl  6650  genpassu  6651  ltexprlemell  6724  ltexprlemelu  6725  ltexprlemm  6726  recexprlemell  6748  recexprlemelu  6749  sumeq1  10068  bdsep2  10336  bdzfauscl  10340  strcoll2  10438