This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY Predicate calculus with equality: Auxiliary axiom schemes (4 schemes) Axiom scheme ax-12 (Substitution) drex1v
Description: Formula-building lemma for use with the Distinctor Reduction Theorem.
Version of drex1 with a disjoint variable condition, which does not
require ax-13 . (Contributed by NM , 27-Feb-2005) (Revised by BJ , 17-Jun-2019)
Ref
Expression
Hypothesis
dral1v.1 ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion
drex1v ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 𝜑 ↔ ∃ 𝑦 𝜓 ) )
Proof
Step
Hyp
Ref
Expression
1
dral1v.1 ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2
1
notbid ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ¬ 𝜑 ↔ ¬ 𝜓 ) )
3
2
dral1v ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 ¬ 𝜑 ↔ ∀ 𝑦 ¬ 𝜓 ) )
4
3
notbid ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ¬ ∀ 𝑥 ¬ 𝜑 ↔ ¬ ∀ 𝑦 ¬ 𝜓 ) )
5
df-ex ⊢ ( ∃ 𝑥 𝜑 ↔ ¬ ∀ 𝑥 ¬ 𝜑 )
6
df-ex ⊢ ( ∃ 𝑦 𝜓 ↔ ¬ ∀ 𝑦 ¬ 𝜓 )
7
4 5 6
3bitr4g ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 𝜑 ↔ ∃ 𝑦 𝜓 ) )