Metamath Proof Explorer


Theorem drex2

Description: Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of Megill p. 448 (p. 16 of preprint). Usage of this theorem is discouraged because it depends on ax-13 . Usage of exbidv is preferred, which requires fewer axioms. (Contributed by NM, 27-Feb-2005) (New usage is discouraged.)

Ref Expression
Hypothesis dral1.1 ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
Assertion drex2 ( ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑧 𝜑 ↔ ∃ 𝑧 𝜓 ) )

Proof

Step Hyp Ref Expression
1 dral1.1 ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
2 nfae 𝑧𝑥 𝑥 = 𝑦
3 2 1 exbid ( ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑧 𝜑 ↔ ∃ 𝑧 𝜓 ) )