Theorem mobidv 2549

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540  ∃*wmo 2537

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 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-mo 2539

This theorem is referenced by:  moanimv  2619  rmobidva  3355  mosubopt  5464  dffun6f  6513  funmo  6514  caovmo  7604  1stconst  8050  2ndconst  8051  brdom3  10450  brdom6disj  10454  imasaddfnlem  17492  imasvscafn  17501  hausflim  23946  hausflf  23962  cnextfun  24029  haustsms  24101  limcmo  25849  perfdvf  25870  rmounid  32564  rmoeqbidv  36395  disjeq12dv  36397  phpreu  37925  alrmomodm  38680  funressnfv  47491  funressnmo  47494  mosn  49288  mof02  49314  mofsn2  49320  f1omo  49368  f1omoOLD  49369  isthinc  49894  isthincd2lem1  49900  thincmoALT  49904  thincmod  49905  isthincd  49911  thincpropd  49917  indcthing  49935  discthing  49936  setcthin  49940