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

Metamath Proof Explorer

Theorem rexraleqim

Description: Statement following from existence and generalization with equality. (Contributed by AV, 9-Feb-2019)

Ref Expression
Hypotheses rexraleqim.1 ⊢ ( 𝑥 = 𝑧 → ( 𝜓 ↔ 𝜑 ) )
rexraleqim.2 ⊢ ( 𝑧 = 𝑌 → ( 𝜑 ↔ 𝜃 ) )
Assertion rexraleqim ( ( ∃ 𝑧 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑌 ) ) → 𝜃 )

Proof

Step Hyp Ref Expression
1 rexraleqim.1 ⊢ ( 𝑥 = 𝑧 → ( 𝜓 ↔ 𝜑 ) )
2 rexraleqim.2 ⊢ ( 𝑧 = 𝑌 → ( 𝜑 ↔ 𝜃 ) )
3 eqeq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 = 𝑌 ↔ 𝑧 = 𝑌 ) )
4 1 3 imbi12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝜓 → 𝑥 = 𝑌 ) ↔ ( 𝜑 → 𝑧 = 𝑌 ) ) )
5 4 rspcva ⊢ ( ( 𝑧 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑌 ) ) → ( 𝜑 → 𝑧 = 𝑌 ) )
6 2 biimpd ⊢ ( 𝑧 = 𝑌 → ( 𝜑 → 𝜃 ) )
7 5 6 syli ⊢ ( ( 𝑧 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑌 ) ) → ( 𝜑 → 𝜃 ) )
8 7 impancom ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝜑 ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑌 ) → 𝜃 ) )
9 8 rexlimiva ⊢ ( ∃ 𝑧 ∈ 𝐴 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑌 ) → 𝜃 ) )
10 9 imp ⊢ ( ( ∃ 𝑧 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑌 ) ) → 𝜃 )