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

Metamath Proof Explorer

Theorem cbvrabv2

Description: A more general version of cbvrabv . Usage of this theorem is discouraged because it depends on ax-13 . Use of cbvrabv2w is preferred. (Contributed by Glauco Siliprandi, 23-Oct-2021) (New usage is discouraged.)

Ref Expression
Hypotheses cbvrabv2.1 ⊢ x = y → A = B
cbvrabv2.2 ⊢ x = y → φ ↔ ψ
Assertion cbvrabv2 ⊢ x ∈ A | φ = y ∈ B | ψ

Proof

Step Hyp Ref Expression
1 cbvrabv2.1 ⊢ x = y → A = B
2 cbvrabv2.2 ⊢ x = y → φ ↔ ψ
3 nfcv ⊢ Ⅎ _ y A
4 nfcv ⊢ Ⅎ _ x B
5 nfv ⊢ Ⅎ y φ
6 nfv ⊢ Ⅎ x ψ
7 3 4 5 6 1 2 cbvrabcsf ⊢ x ∈ A | φ = y ∈ B | ψ