Theorem mobidv 2543

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1539  ∃*wmo 2532

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 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-mo 2534

This theorem is referenced by:  moanimv  2615  rmobidva  3391  rmoeq1OLD  3416  mosubopt  5510  dffun6f  6561  funmo  6563  funmoOLD  6564  caovmo  7646  1stconst  8088  2ndconst  8089  brdom3  10525  brdom6disj  10529  imasaddfnlem  17478  imasvscafn  17487  hausflim  23705  hausflf  23721  cnextfun  23788  haustsms  23860  limcmo  25623  perfdvf  25644  rmounid  31990  phpreu  36775  alrmomodm  37531  funressnfv  46052  funressnmo  46055  mosn  47585  mof02  47593  mofsn2  47599  f1omo  47615  isthinc  47729  isthincd2lem1  47735  thincmoALT  47738  thincmod  47739  isthincd  47745  setcthin  47763