rexopabb

Description: Restricted existential quantification over an ordered-pair class abstraction. (Contributed by AV, 8-Nov-2023)

	Ref	Expression
Hypotheses	rexopabb.o	⊢ 𝑂 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
	rexopabb.p	⊢ ( 𝑜 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜓 ↔ 𝜒 ) )
Assertion	rexopabb	⊢ ( ∃ 𝑜 ∈ 𝑂 𝜓 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝜑 ∧ 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		rexopabb.o	⊢ 𝑂 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
2		rexopabb.p	⊢ ( 𝑜 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜓 ↔ 𝜒 ) )
3	1	rexeqi	⊢ ( ∃ 𝑜 ∈ 𝑂 𝜓 ↔ ∃ 𝑜 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝜓 )
4		elopab	⊢ ( 𝑜 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑜 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
5		simprr	⊢ ( ( 𝜓 ∧ ( 𝑜 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) → 𝜑 )
6	2	biimpd	⊢ ( 𝑜 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜓 → 𝜒 ) )
7	6	adantr	⊢ ( ( 𝑜 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → ( 𝜓 → 𝜒 ) )
8	7	impcom	⊢ ( ( 𝜓 ∧ ( 𝑜 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) → 𝜒 )
9	5 8	jca	⊢ ( ( 𝜓 ∧ ( 𝑜 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) → ( 𝜑 ∧ 𝜒 ) )
10	9	ex	⊢ ( 𝜓 → ( ( 𝑜 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → ( 𝜑 ∧ 𝜒 ) ) )
11	10	2eximdv	⊢ ( 𝜓 → ( ∃ 𝑥 ∃ 𝑦 ( 𝑜 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → ∃ 𝑥 ∃ 𝑦 ( 𝜑 ∧ 𝜒 ) ) )
12	11	impcom	⊢ ( ( ∃ 𝑥 ∃ 𝑦 ( 𝑜 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ∧ 𝜓 ) → ∃ 𝑥 ∃ 𝑦 ( 𝜑 ∧ 𝜒 ) )
13	4 12	sylanb	⊢ ( ( 𝑜 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∧ 𝜓 ) → ∃ 𝑥 ∃ 𝑦 ( 𝜑 ∧ 𝜒 ) )
14	13	rexlimiva	⊢ ( ∃ 𝑜 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝜓 → ∃ 𝑥 ∃ 𝑦 ( 𝜑 ∧ 𝜒 ) )
15		nfopab1	⊢ Ⅎ 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
16		nfv	⊢ Ⅎ 𝑥 𝜓
17	15 16	nfrexw	⊢ Ⅎ 𝑥 ∃ 𝑜 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝜓
18		nfopab2	⊢ Ⅎ 𝑦 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
19		nfv	⊢ Ⅎ 𝑦 𝜓
20	18 19	nfrexw	⊢ Ⅎ 𝑦 ∃ 𝑜 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝜓
21		opabidw	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ 𝜑 )
22		opex	⊢ ⟨ 𝑥 , 𝑦 ⟩ ∈ V
23	22 2	sbcie	⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ / 𝑜 ] 𝜓 ↔ 𝜒 )
24		rspesbca	⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∧ [ ⟨ 𝑥 , 𝑦 ⟩ / 𝑜 ] 𝜓 ) → ∃ 𝑜 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝜓 )
25	21 23 24	syl2anbr	⊢ ( ( 𝜑 ∧ 𝜒 ) → ∃ 𝑜 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝜓 )
26	20 25	exlimi	⊢ ( ∃ 𝑦 ( 𝜑 ∧ 𝜒 ) → ∃ 𝑜 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝜓 )
27	17 26	exlimi	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝜑 ∧ 𝜒 ) → ∃ 𝑜 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝜓 )
28	14 27	impbii	⊢ ( ∃ 𝑜 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝜓 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝜑 ∧ 𝜒 ) )
29	3 28	bitri	⊢ ( ∃ 𝑜 ∈ 𝑂 𝜓 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝜑 ∧ 𝜒 ) )

Metamath Proof Explorer

Theorem rexopabb

Proof