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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537  ∃*wmo 2538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-mo 2540

This theorem is referenced by:  moanimv  2621  rmobidva  3327  rmoeq1  3345  mosubopt  5424  dffun6f  6448  funmo  6450  caovmo  7509  1stconst  7940  2ndconst  7941  brdom3  10284  brdom6disj  10288  imasaddfnlem  17239  imasvscafn  17248  hausflim  23132  hausflf  23148  cnextfun  23215  haustsms  23287  limcmo  25046  perfdvf  25067  rmounid  30843  phpreu  35761  alrmomodm  36491  funressnfv  44537  funressnmo  44540  mosn  46158  mof02  46166  mofsn2  46172  f1omo  46188  isthinc  46302  isthincd2lem1  46308  thincmoALT  46311  thincmod  46312  isthincd  46318  setcthin  46336