Theorem mobidv 2546

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

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

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 2537

This theorem is referenced by:  moanimv  2616  rmobidva  3360  rmoeq1OLD  3380  mosubopt  5453  dffun6f  6501  funmo  6502  caovmo  7589  1stconst  8036  2ndconst  8037  brdom3  10426  brdom6disj  10430  imasaddfnlem  17434  imasvscafn  17443  hausflim  23897  hausflf  23913  cnextfun  23980  haustsms  24052  limcmo  25811  perfdvf  25832  rmounid  32476  rmoeqbidv  36278  disjeq12dv  36280  phpreu  37664  alrmomodm  38411  funressnfv  47167  funressnmo  47170  mosn  48937  mof02  48963  mofsn2  48969  f1omo  49017  f1omoOLD  49018  isthinc  49544  isthincd2lem1  49550  thincmoALT  49554  thincmod  49555  isthincd  49561  thincpropd  49567  indcthing  49585  discthing  49586  setcthin  49590