Theorem mobidv 2576

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

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

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 2566

This theorem is used by:  moanimv  2646  rmobidva  3380  mosubopt  5491  dffun6f  6552  funmo  6553  caovmo  7655  1stconst  8101  2ndconst  8102  brdom3  10535  brdom6disj  10539  imasaddfnlem  17620  imasvscafn  17629  hausflim  24213  hausflf  24229  cnextfun  24296  haustsms  24368  limcmo  26116  perfdvf  26137  rmounid  32978  rmoeqbidv  36841  disjeq12dv  36843  phpreu  38366  alrmomodm  39115  funressnfv  47939  funressnmo  47942  mosn  49749  mof02  49775  mofsn2  49781  f1omo  49827  f1omoOLD  49828  isthinc  50353  isthincd2lem1  50359  thincmoALT  50363  thincmod  50364  isthincd  50370  thincpropd  50376  indcthing  50394  discthing  50395  setcthin  50399