Theorem fvpr2OLD

Description: Obsolete version of fvpr2 as of 26-Sep-2024. (Contributed by Jeff Madsen, 20-Jun-2010) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	fvpr2.1	⊢ 𝐵 ∈ V
	fvpr2.2	⊢ 𝐷 ∈ V
Assertion	fvpr2OLD	⊢ ( 𝐴 ≠ 𝐵 → ( { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ‘ 𝐵 ) = 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		fvpr2.1	⊢ 𝐵 ∈ V
2		fvpr2.2	⊢ 𝐷 ∈ V
3		prcom	⊢ { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = { ⟨ 𝐵 , 𝐷 ⟩ , ⟨ 𝐴 , 𝐶 ⟩ }
4	3	fveq1i	⊢ ( { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ‘ 𝐵 ) = ( { ⟨ 𝐵 , 𝐷 ⟩ , ⟨ 𝐴 , 𝐶 ⟩ } ‘ 𝐵 )
5		necom	⊢ ( 𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴 )
6	1 2	fvpr1	⊢ ( 𝐵 ≠ 𝐴 → ( { ⟨ 𝐵 , 𝐷 ⟩ , ⟨ 𝐴 , 𝐶 ⟩ } ‘ 𝐵 ) = 𝐷 )
7	5 6	sylbi	⊢ ( 𝐴 ≠ 𝐵 → ( { ⟨ 𝐵 , 𝐷 ⟩ , ⟨ 𝐴 , 𝐶 ⟩ } ‘ 𝐵 ) = 𝐷 )
8	4 7	syl5eq	⊢ ( 𝐴 ≠ 𝐵 → ( { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ‘ 𝐵 ) = 𝐷 )