Theorem mobidv 2544

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

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

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 2535

This theorem is referenced by:  moanimv  2614  rmobidva  3359  rmoeq1OLD  3379  mosubopt  5450  dffun6f  6496  funmo  6497  caovmo  7583  1stconst  8030  2ndconst  8031  brdom3  10416  brdom6disj  10420  imasaddfnlem  17429  imasvscafn  17438  hausflim  23894  hausflf  23910  cnextfun  23977  haustsms  24049  limcmo  25808  perfdvf  25829  rmounid  32469  rmoeqbidv  36246  disjeq12dv  36248  phpreu  37643  alrmomodm  38386  funressnfv  47073  funressnmo  47076  mosn  48843  mof02  48869  mofsn2  48875  f1omo  48923  f1omoOLD  48924  isthinc  49450  isthincd2lem1  49456  thincmoALT  49460  thincmod  49461  isthincd  49467  thincpropd  49473  indcthing  49491  discthing  49492  setcthin  49496