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	⊢ ( ( ∃ 𝑧 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝑥 = 𝑌 ) ) → 𝜃 )