Theorem mobidv 2553

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

Syntax hints:   → wi 4   ↔ wb 207  ∀wal 1545  ∃*wmo 2541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-mo 2543

This theorem is referenced by:  moanimv  2623  rmobidva  3358  mosubopt  5458  dffun6f  6507  funmo  6508  caovmo  7600  1stconst  8046  2ndconst  8047  brdom3  10448  brdom6disj  10452  imasaddfnlem  17490  imasvscafn  17499  hausflim  23971  hausflf  23987  cnextfun  24054  haustsms  24126  limcmo  25874  perfdvf  25895  rmounid  32589  rmoeqbidv  36448  disjeq12dv  36450  phpreu  37978  alrmomodm  38733  funressnfv  47513  funressnmo  47516  mosn  49310  mof02  49336  mofsn2  49342  f1omo  49390  f1omoOLD  49391  isthinc  49916  isthincd2lem1  49922  thincmoALT  49926  thincmod  49927  isthincd  49933  thincpropd  49939  indcthing  49957  discthing  49958  setcthin  49962