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

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

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 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-mo 2534

This theorem is referenced by:  moanimv  2615  rmobidva  3391  rmoeq1OLD  3416  mosubopt  5509  dffun6f  6558  funmo  6560  funmoOLD  6561  caovmo  7640  1stconst  8082  2ndconst  8083  brdom3  10519  brdom6disj  10523  imasaddfnlem  17470  imasvscafn  17479  hausflim  23476  hausflf  23492  cnextfun  23559  haustsms  23631  limcmo  25390  perfdvf  25411  rmounid  31722  phpreu  36460  alrmomodm  37216  funressnfv  45739  funressnmo  45742  mosn  47450  mof02  47458  mofsn2  47464  f1omo  47480  isthinc  47594  isthincd2lem1  47600  thincmoALT  47603  thincmod  47604  isthincd  47610  setcthin  47628