Theorem mobidv 2548

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1541  ∃*wmo 2537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-mo 2539

This theorem is referenced by:  moanimv  2620  rmoeq1  3312  mosubopt  5378  dffun6f  6372  funmo  6374  caovmo  7423  1stconst  7846  2ndconst  7847  brdom3  10107  brdom6disj  10111  imasaddfnlem  16987  imasvscafn  16996  hausflim  22832  hausflf  22848  cnextfun  22915  haustsms  22987  limcmo  24733  perfdvf  24754  rmounid  30516  phpreu  35447  alrmomodm  36177  funressnfv  44152  funressnmo  44155  mosn  45774  mof02  45782  mofsn2  45788  f1omo  45804  isthinc  45918  isthincd2lem1  45924  thincmoALT  45927  thincmod  45928  isthincd  45934  setcthin  45952