Theorem prtlem5

Description: Lemma for prter1 , prter2 , prter3 and prtex . (Contributed by Rodolfo Medina, 25-Sep-2010) (Proof shortened by Mario Carneiro, 11-Dec-2016)

	Ref	Expression
Assertion	prtlem5	⊢ ( [ 𝑠 / 𝑣 ] [ 𝑟 / 𝑢 ] ∃ 𝑥 ∈ 𝐴 ( 𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐴 ( 𝑟 ∈ 𝑥 ∧ 𝑠 ∈ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		elequ1	⊢ ( 𝑢 = 𝑟 → ( 𝑢 ∈ 𝑥 ↔ 𝑟 ∈ 𝑥 ) )
2		elequ1	⊢ ( 𝑣 = 𝑠 → ( 𝑣 ∈ 𝑥 ↔ 𝑠 ∈ 𝑥 ) )
3	1 2	bi2anan9r	⊢ ( ( 𝑣 = 𝑠 ∧ 𝑢 = 𝑟 ) → ( ( 𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥 ) ↔ ( 𝑟 ∈ 𝑥 ∧ 𝑠 ∈ 𝑥 ) ) )
4	3	rexbidv	⊢ ( ( 𝑣 = 𝑠 ∧ 𝑢 = 𝑟 ) → ( ∃ 𝑥 ∈ 𝐴 ( 𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐴 ( 𝑟 ∈ 𝑥 ∧ 𝑠 ∈ 𝑥 ) ) )
5	4	2sbievw	⊢ ( [ 𝑠 / 𝑣 ] [ 𝑟 / 𝑢 ] ∃ 𝑥 ∈ 𝐴 ( 𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐴 ( 𝑟 ∈ 𝑥 ∧ 𝑠 ∈ 𝑥 ) )