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	⊢ ( 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜓 ↔ 𝜑 ) )
	cnvoprab.2	⊢ ( 𝜓 → 𝑎 ∈ ( V × V ) )
Assertion	cnvoprab	⊢ ◡ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ 𝑧 , 𝑎 ⟩ ∣ 𝜓 }

Proof

Step	Hyp	Ref	Expression
1		cnvoprab.1	⊢ ( 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜓 ↔ 𝜑 ) )
2		cnvoprab.2	⊢ ( 𝜓 → 𝑎 ∈ ( V × V ) )
3	1	dfoprab3	⊢ { ⟨ 𝑎 , 𝑧 ⟩ ∣ ( 𝑎 ∈ ( V × V ) ∧ 𝜓 ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 }
4	3	cnveqi	⊢ ◡ { ⟨ 𝑎 , 𝑧 ⟩ ∣ ( 𝑎 ∈ ( V × V ) ∧ 𝜓 ) } = ◡ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 }
5		cnvopab	⊢ ◡ { ⟨ 𝑎 , 𝑧 ⟩ ∣ ( 𝑎 ∈ ( V × V ) ∧ 𝜓 ) } = { ⟨ 𝑧 , 𝑎 ⟩ ∣ ( 𝑎 ∈ ( V × V ) ∧ 𝜓 ) }
6		inopab	⊢ ( { ⟨ 𝑧 , 𝑎 ⟩ ∣ 𝑎 ∈ ( V × V ) } ∩ { ⟨ 𝑧 , 𝑎 ⟩ ∣ 𝜓 } ) = { ⟨ 𝑧 , 𝑎 ⟩ ∣ ( 𝑎 ∈ ( V × V ) ∧ 𝜓 ) }
7	2	ssopab2i	⊢ { ⟨ 𝑧 , 𝑎 ⟩ ∣ 𝜓 } ⊆ { ⟨ 𝑧 , 𝑎 ⟩ ∣ 𝑎 ∈ ( V × V ) }
8		sseqin2	⊢ ( { ⟨ 𝑧 , 𝑎 ⟩ ∣ 𝜓 } ⊆ { ⟨ 𝑧 , 𝑎 ⟩ ∣ 𝑎 ∈ ( V × V ) } ↔ ( { ⟨ 𝑧 , 𝑎 ⟩ ∣ 𝑎 ∈ ( V × V ) } ∩ { ⟨ 𝑧 , 𝑎 ⟩ ∣ 𝜓 } ) = { ⟨ 𝑧 , 𝑎 ⟩ ∣ 𝜓 } )
9	7 8	mpbi	⊢ ( { ⟨ 𝑧 , 𝑎 ⟩ ∣ 𝑎 ∈ ( V × V ) } ∩ { ⟨ 𝑧 , 𝑎 ⟩ ∣ 𝜓 } ) = { ⟨ 𝑧 , 𝑎 ⟩ ∣ 𝜓 }
10	5 6 9	3eqtr2i	⊢ ◡ { ⟨ 𝑎 , 𝑧 ⟩ ∣ ( 𝑎 ∈ ( V × V ) ∧ 𝜓 ) } = { ⟨ 𝑧 , 𝑎 ⟩ ∣ 𝜓 }
11	4 10	eqtr3i	⊢ ◡ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ 𝑧 , 𝑎 ⟩ ∣ 𝜓 }