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

Metamath Proof Explorer

Theorem ovmpodv

Description: Alternate deduction version of ovmpo , suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017)

Ref Expression
Hypotheses ovmpodf.1 ⊢ φ → A ∈ C
ovmpodf.2 ⊢ φ ∧ x = A → B ∈ D
ovmpodf.3 ⊢ φ ∧ x = A ∧ y = B → R ∈ V
ovmpodf.4 ⊢ φ ∧ x = A ∧ y = B → A F B = R → ψ
Assertion ovmpodv ⊢ φ → F = x ∈ C , y ∈ D ⟼ R → ψ

Proof

Step Hyp Ref Expression
1 ovmpodf.1 ⊢ φ → A ∈ C
2 ovmpodf.2 ⊢ φ ∧ x = A → B ∈ D
3 ovmpodf.3 ⊢ φ ∧ x = A ∧ y = B → R ∈ V
4 ovmpodf.4 ⊢ φ ∧ x = A ∧ y = B → A F B = R → ψ
5 nfcv ⊢ Ⅎ _ x F
6 nfv ⊢ Ⅎ x ψ
7 nfcv ⊢ Ⅎ _ y F
8 nfv ⊢ Ⅎ y ψ
9 1 2 3 4 5 6 7 8 ovmpodf ⊢ φ → F = x ∈ C , y ∈ D ⟼ R → ψ