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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538  ∃*wmo 2538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-mo 2540

This theorem is referenced by:  moanimv  2619  rmobidva  3395  rmoeq1OLD  3418  mosubopt  5515  dffun6f  6579  funmo  6581  funmoOLD  6582  caovmo  7670  1stconst  8125  2ndconst  8126  brdom3  10568  brdom6disj  10572  imasaddfnlem  17573  imasvscafn  17582  hausflim  23989  hausflf  24005  cnextfun  24072  haustsms  24144  limcmo  25917  perfdvf  25938  rmounid  32514  rmoeqbidv  36214  disjeq12dv  36216  phpreu  37611  alrmomodm  38360  funressnfv  47055  funressnmo  47058  mosn  48732  mof02  48748  mofsn2  48754  f1omo  48792  isthinc  49069  isthincd2lem1  49075  thincmoALT  49078  thincmod  49079  isthincd  49085  thincpropd  49091  setcthin  49112