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 Restricted quantification Restricted universal and existential quantification raleleqOLD
Description: Obsolete version of raleleq as of 18-Jul-2025. (Contributed by AV , 30-Oct-2020) (Proof modification is discouraged.)
(New usage is discouraged.)
Ref
Expression
Assertion
raleleqOLD ⊢ ( 𝐴 = 𝐵 → ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 )
Proof
Step
Hyp
Ref
Expression
1
ralel ⊢ ∀ 𝑥 ∈ 𝐵 𝑥 ∈ 𝐵
2
id ⊢ ( 𝐴 = 𝐵 → 𝐴 = 𝐵 )
3
2
raleqdv ⊢ ( 𝐴 = 𝐵 → ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ↔ ∀ 𝑥 ∈ 𝐵 𝑥 ∈ 𝐵 ) )
4
1 3
mpbiri ⊢ ( 𝐴 = 𝐵 → ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 )