This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality The universal class rspcedvdw
Description: Version of rspcedvd where the implicit substitution hypothesis does
not have an antecedent, which also avoids a disjoint variable condition
on ph , x . (Contributed by SN , 20-Aug-2024)
Ref
Expression
Hypotheses
rspcedvdw.s ⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜒 ) )
rspcedvdw.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
rspcedvdw.2 ⊢ ( 𝜑 → 𝜒 )
Assertion
rspcedvdw ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 𝜓 )
Proof
Step
Hyp
Ref
Expression
1
rspcedvdw.s ⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜒 ) )
2
rspcedvdw.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
3
rspcedvdw.2 ⊢ ( 𝜑 → 𝜒 )
4
1
rspcev ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝜒 ) → ∃ 𝑥 ∈ 𝐵 𝜓 )
5
2 3 4
syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 𝜓 )