This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nfrex

Description: Bound-variable hypothesis builder for restricted quantification. Usage of this theorem is discouraged because it depends on ax-13 . See nfrexw for a version with a disjoint variable condition, but not requiring ax-13 . (Contributed by NM, 1-Sep-1999) (Revised by Mario Carneiro, 7-Oct-2016) (Proof shortened by Wolf Lammen, 30-Dec-2019) (New usage is discouraged.)

Ref Expression
Hypotheses nfral.1 ⊢ Ⅎ _ x A
nfral.2 ⊢ Ⅎ x φ
Assertion nfrex ⊢ Ⅎ x ∃ y ∈ A φ

Proof

Step Hyp Ref Expression
1 nfral.1 ⊢ Ⅎ _ x A
2 nfral.2 ⊢ Ⅎ x φ
3 nftru ⊢ Ⅎ y ⊤
4 1 a1i ⊢ ⊤ → Ⅎ _ x A
5 2 a1i ⊢ ⊤ → Ⅎ x φ
6 3 4 5 nfrexd ⊢ ⊤ → Ⅎ x ∃ y ∈ A φ
7 6 mptru ⊢ Ⅎ x ∃ y ∈ A φ