Theorem mobidv 2575

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568  ∃*wmo 2563

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-mo 2565

This theorem is used by:  moanimv  2645  rmobidva  3379  mosubopt  5482  mosubott  5484  dffun6f  6546  funmo  6547  caovmo  7650  1stconst  8100  2ndconst  8101  brdom3  10588  brdom6disj  10592  imasaddfnlem  17680  imasvscafn  17689  hausflim  24280  hausflf  24296  cnextfun  24363  haustsms  24435  limcmo  26182  perfdvf  26203  rmounid  33073  rmoeqbidv  36972  disjeq12dv  36974  phpreu  38495  alrmomodm  39259  funressnfv  48057  funressnmo  48060  mosn  49867  mof02  49893  mofsn2  49899  f1omo  49945  f1omoOLD  49946  isthinc  50471  isthincd2lem1  50477  thincmoALT  50481  thincmod  50482  isthincd  50488  thincpropd  50494  indcthing  50512  discthing  50513  setcthin  50517