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

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1557  ∃*wmo 2563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-mo 2565

This theorem is referenced by:  moanimv  2645  rmobidva  3379  mosubopt  5478  dffun6f  6532  funmo  6533  caovmo  7629  1stconst  8074  2ndconst  8075  brdom3  10482  brdom6disj  10486  imasaddfnlem  17541  imasvscafn  17550  hausflim  24021  hausflf  24037  cnextfun  24104  haustsms  24176  limcmo  25924  perfdvf  25945  rmounid  32642  rmoeqbidv  36537  disjeq12dv  36539  phpreu  38067  alrmomodm  38822  funressnfv  47601  funressnmo  47604  mosn  49398  mof02  49424  mofsn2  49430  f1omo  49478  f1omoOLD  49479  isthinc  50004  isthincd2lem1  50010  thincmoALT  50014  thincmod  50015  isthincd  50021  thincpropd  50027  indcthing  50045  discthing  50046  setcthin  50050