Theorem cllem0

Description: The class of all sets with property ph ( z ) is closed under the binary operation on sets defined in R ( x , y ) . (Contributed by RP, 3-Jan-2020)

	Ref	Expression
Hypotheses	cllem0.v	⊢ 𝑉 = { 𝑧 ∣ 𝜑 }
	cllem0.rex	⊢ 𝑅 ∈ 𝑈
	cllem0.r	⊢ ( 𝑧 = 𝑅 → ( 𝜑 ↔ 𝜓 ) )
	cllem0.x	⊢ ( 𝑧 = 𝑥 → ( 𝜑 ↔ 𝜒 ) )
	cllem0.y	⊢ ( 𝑧 = 𝑦 → ( 𝜑 ↔ 𝜃 ) )
	cllem0.closed	⊢ ( ( 𝜒 ∧ 𝜃 ) → 𝜓 )
Assertion	cllem0	⊢ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 𝑅 ∈ 𝑉

Proof

Step	Hyp	Ref	Expression
1		cllem0.v	⊢ 𝑉 = { 𝑧 ∣ 𝜑 }
2		cllem0.rex	⊢ 𝑅 ∈ 𝑈
3		cllem0.r	⊢ ( 𝑧 = 𝑅 → ( 𝜑 ↔ 𝜓 ) )
4		cllem0.x	⊢ ( 𝑧 = 𝑥 → ( 𝜑 ↔ 𝜒 ) )
5		cllem0.y	⊢ ( 𝑧 = 𝑦 → ( 𝜑 ↔ 𝜃 ) )
6		cllem0.closed	⊢ ( ( 𝜒 ∧ 𝜃 ) → 𝜓 )
7	2	elexi	⊢ 𝑅 ∈ V
8	7 3 1	elab2	⊢ ( 𝑅 ∈ 𝑉 ↔ 𝜓 )
9	8	ralbii	⊢ ( ∀ 𝑦 ∈ 𝑉 𝑅 ∈ 𝑉 ↔ ∀ 𝑦 ∈ 𝑉 𝜓 )
10	9	ralbii	⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 𝑅 ∈ 𝑉 ↔ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 𝜓 )
11		df-ral	⊢ ( ∀ 𝑦 ∈ 𝑉 𝜓 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑉 → 𝜓 ) )
12	11	ralbii	⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 𝜓 ↔ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ( 𝑦 ∈ 𝑉 → 𝜓 ) )
13		df-ral	⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ( 𝑦 ∈ 𝑉 → 𝜓 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑉 → ∀ 𝑦 ( 𝑦 ∈ 𝑉 → 𝜓 ) ) )
14	10 12 13	3bitri	⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 𝑅 ∈ 𝑉 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑉 → ∀ 𝑦 ( 𝑦 ∈ 𝑉 → 𝜓 ) ) )
15		vex	⊢ 𝑥 ∈ V
16	15 4 1	elab2	⊢ ( 𝑥 ∈ 𝑉 ↔ 𝜒 )
17		vex	⊢ 𝑦 ∈ V
18	17 5 1	elab2	⊢ ( 𝑦 ∈ 𝑉 ↔ 𝜃 )
19	16 18 6	syl2anb	⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → 𝜓 )
20	19	ex	⊢ ( 𝑥 ∈ 𝑉 → ( 𝑦 ∈ 𝑉 → 𝜓 ) )
21	20	alrimiv	⊢ ( 𝑥 ∈ 𝑉 → ∀ 𝑦 ( 𝑦 ∈ 𝑉 → 𝜓 ) )
22	14 21	mpgbir	⊢ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 𝑅 ∈ 𝑉