Theorem mobidv 2550

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 1929	. 2 ⊢ (𝜑 → ∀𝑥(𝜓 ↔ 𝜒))
3		mobi 2548	. 2 ⊢ (∀𝑥(𝜓 ↔ 𝜒) → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
4	2, 3	syl 17	1 ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540  ∃*wmo 2538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-mo 2540

This theorem is referenced by:  moanimv  2620  rmobidva  3356  mosubopt  5458  dffun6f  6507  funmo  6508  caovmo  7597  1stconst  8043  2ndconst  8044  brdom3  10441  brdom6disj  10445  imasaddfnlem  17483  imasvscafn  17492  hausflim  23956  hausflf  23972  cnextfun  24039  haustsms  24111  limcmo  25859  perfdvf  25880  rmounid  32579  rmoeqbidv  36411  disjeq12dv  36413  phpreu  37939  alrmomodm  38694  funressnfv  47503  funressnmo  47506  mosn  49300  mof02  49326  mofsn2  49332  f1omo  49380  f1omoOLD  49381  isthinc  49906  isthincd2lem1  49912  thincmoALT  49916  thincmod  49917  isthincd  49923  thincpropd  49929  indcthing  49947  discthing  49948  setcthin  49952