Theorem mobidv 2543

Description: Formula-building rule for the at-most-one quantifier (deduction form). (Contributed by Mario Carneiro, 7-Oct-2016.) Reduce axiom dependencies and shorten proof. (Revised by BJ, 7-Oct-2022.)

Hypothesis

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

Assertion

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

Distinct variable group:   𝜑,𝑥

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

Proof of Theorem mobidv

Step	Hyp	Ref	Expression
1		mobidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	alrimiv 1928	. 2 ⊢ (𝜑 → ∀𝑥(𝜓 ↔ 𝜒))
3		mobi 2541	. 2 ⊢ (∀𝑥(𝜓 ↔ 𝜒) → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
4	2, 3	syl 17	1 ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539  ∃*wmo 2532

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 207  df-an 396  df-ex 1781  df-mo 2534

This theorem is referenced by:  moanimv  2613  rmobidva  3357  rmoeq1OLD  3377  mosubopt  5448  dffun6f  6492  funmo  6493  caovmo  7578  1stconst  8025  2ndconst  8026  brdom3  10411  brdom6disj  10415  imasaddfnlem  17424  imasvscafn  17433  hausflim  23889  hausflf  23905  cnextfun  23972  haustsms  24044  limcmo  25803  perfdvf  25824  rmounid  32464  rmoeqbidv  36226  disjeq12dv  36228  phpreu  37623  alrmomodm  38366  funressnfv  47053  funressnmo  47056  mosn  48823  mof02  48849  mofsn2  48855  f1omo  48903  f1omoOLD  48904  isthinc  49430  isthincd2lem1  49436  thincmoALT  49440  thincmod  49441  isthincd  49447  thincpropd  49453  indcthing  49471  discthing  49472  setcthin  49476