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

Metamath Proof Explorer

Theorem cnvoprab

Description: The converse of a class abstraction of nested ordered pairs. (Contributed by Thierry Arnoux, 17-Aug-2017) (Proof shortened by Thierry Arnoux, 20-Feb-2022)

Ref Expression
Hypotheses cnvoprab.1 ⊢ a = x y → ψ ↔ φ
cnvoprab.2 ⊢ ψ → a ∈ V × V
Assertion cnvoprab ⊢ x y z | φ -1 = z a | ψ

Proof

Step Hyp Ref Expression
1 cnvoprab.1 ⊢ a = x y → ψ ↔ φ
2 cnvoprab.2 ⊢ ψ → a ∈ V × V
3 1 dfoprab3 ⊢ a z | a ∈ V × V ∧ ψ = x y z | φ
4 3 cnveqi ⊢ a z | a ∈ V × V ∧ ψ -1 = x y z | φ -1
5 cnvopab ⊢ a z | a ∈ V × V ∧ ψ -1 = z a | a ∈ V × V ∧ ψ
6 inopab ⊢ z a | a ∈ V × V ∩ z a | ψ = z a | a ∈ V × V ∧ ψ
7 2 ssopab2i ⊢ z a | ψ ⊆ z a | a ∈ V × V
8 sseqin2 ⊢ z a | ψ ⊆ z a | a ∈ V × V ↔ z a | a ∈ V × V ∩ z a | ψ = z a | ψ
9 7 8 mpbi ⊢ z a | a ∈ V × V ∩ z a | ψ = z a | ψ
10 5 6 9 3eqtr2i ⊢ a z | a ∈ V × V ∧ ψ -1 = z a | ψ
11 4 10 eqtr3i ⊢ x y z | φ -1 = z a | ψ