Theorem onfrALTlem5VD 41591

Description: Virtual deduction proof of onfrALTlem5 41248. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. onfrALTlem5 41248 is onfrALTlem5VD 41591 without virtual deductions and was automatically derived from onfrALTlem5VD 41591.

1::	⊢ 𝑎 ∈ V
2:1:	⊢ (𝑎 ∩ 𝑥) ∈ V
3:2:	⊢ ([(𝑎 ∩ 𝑥) / 𝑏]𝑏 = ∅ ↔ (𝑎 ∩ 𝑥) = ∅)
4:3:	⊢ (¬ [(𝑎 ∩ 𝑥) / 𝑏]𝑏 = ∅ ↔ ¬ (𝑎 ∩ 𝑥) = ∅)
5::	⊢ ((𝑎 ∩ 𝑥) ≠ ∅ ↔ ¬ (𝑎 ∩ 𝑥 ) = ∅)
6:4,5:	⊢ (¬ [(𝑎 ∩ 𝑥) / 𝑏]𝑏 = ∅ ↔ (𝑎 ∩ 𝑥) ≠ ∅)
7:2:	⊢ (¬ [(𝑎 ∩ 𝑥) / 𝑏]𝑏 = ∅ ↔ [(𝑎 ∩ 𝑥) / 𝑏]¬ 𝑏 = ∅)
8::	⊢ (𝑏 ≠ ∅ ↔ ¬ 𝑏 = ∅)
9:8:	⊢ ∀𝑏(𝑏 ≠ ∅ ↔ ¬ 𝑏 = ∅)
10:2,9:	⊢ ([(𝑎 ∩ 𝑥) / 𝑏]𝑏 ≠ ∅ ↔ [(𝑎 ∩ 𝑥) / 𝑏]¬ 𝑏 = ∅)
11:7,10:	⊢ (¬ [(𝑎 ∩ 𝑥) / 𝑏]𝑏 = ∅ ↔ [(𝑎 ∩ 𝑥) / 𝑏]𝑏 ≠ ∅)
12:6,11:	⊢ ([(𝑎 ∩ 𝑥) / 𝑏]𝑏 ≠ ∅ ↔ ( 𝑎 ∩ 𝑥) ≠ ∅)
13:2:	⊢ ([(𝑎 ∩ 𝑥) / 𝑏]𝑏 ⊆ (𝑎 ∩ 𝑥 ) ↔ (𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥))
14:12,13:	⊢ (([(𝑎 ∩ 𝑥) / 𝑏]𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ [(𝑎 ∩ 𝑥) / 𝑏]𝑏 ≠ ∅) ↔ ((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅))
15:2:	⊢ ([(𝑎 ∩ 𝑥) / 𝑏](𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) ↔ ([(𝑎 ∩ 𝑥) / 𝑏]𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ [(𝑎 ∩ 𝑥) / 𝑏]𝑏 ≠ ∅))
16:15,14:	⊢ ([(𝑎 ∩ 𝑥) / 𝑏](𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) ↔ ((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅))
17:2:	⊢ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌(𝑏 ∩ 𝑦) = ( ⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑏 ∩ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑦)
18:2:	⊢ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑏 = (𝑎 ∩ 𝑥)
19:2:	⊢ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑦 = 𝑦
20:18,19:	⊢ (⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑏 ∩ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑦) = ((𝑎 ∩ 𝑥) ∩ 𝑦)
21:17,20:	⊢ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌(𝑏 ∩ 𝑦) = (( 𝑎 ∩ 𝑥) ∩ 𝑦)
22:2:	⊢ ([(𝑎 ∩ 𝑥) / 𝑏](𝑏 ∩ 𝑦) = ∅ ↔ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌(𝑏 ∩ 𝑦) = ⦋(𝑎 ∩ 𝑥) / 𝑏⦌ ∅)
23:2:	⊢ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌∅ = ∅
24:21,23:	⊢ (⦋(𝑎 ∩ 𝑥) / 𝑏⦌(𝑏 ∩ 𝑦) = ⦋(𝑎 ∩ 𝑥) / 𝑏⦌∅ ↔ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)
25:22,24:	⊢ ([(𝑎 ∩ 𝑥) / 𝑏](𝑏 ∩ 𝑦) = ∅ ↔ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)
26:2:	⊢ ([(𝑎 ∩ 𝑥) / 𝑏]𝑦 ∈ 𝑏 ↔ 𝑦 ∈ (𝑎 ∩ 𝑥))
27:25,26:	⊢ (([(𝑎 ∩ 𝑥) / 𝑏]𝑦 ∈ 𝑏 ∧ [ (𝑎 ∩ 𝑥) / 𝑏](𝑏 ∩ 𝑦) = ∅) ↔ (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ (( 𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))
28:2:	⊢ ([(𝑎 ∩ 𝑥) / 𝑏](𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅) ↔ ([(𝑎 ∩ 𝑥) / 𝑏]𝑦 ∈ 𝑏 ∧ [(𝑎 ∩ 𝑥) / 𝑏](𝑏 ∩ 𝑦) = ∅))
29:27,28:	⊢ ([(𝑎 ∩ 𝑥) / 𝑏](𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅) ↔ (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))
30:29:	⊢ ∀𝑦([(𝑎 ∩ 𝑥) / 𝑏](𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅) ↔ (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))
31:30:	⊢ (∃𝑦[(𝑎 ∩ 𝑥) / 𝑏](𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅) ↔ ∃𝑦(𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))
32::	⊢ (∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅ ↔ ∃𝑦(𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅ ))
33:31,32:	⊢ (∃𝑦[(𝑎 ∩ 𝑥) / 𝑏](𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅) ↔ ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)
34:2:	⊢ (∃𝑦[(𝑎 ∩ 𝑥) / 𝑏](𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅) ↔ [(𝑎 ∩ 𝑥) / 𝑏]∃𝑦(𝑦 ∈ 𝑏 ∧ ( 𝑏 ∩ 𝑦) = ∅))
35:33,34:	⊢ ([(𝑎 ∩ 𝑥) / 𝑏]∃𝑦(𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅) ↔ ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦 ) = ∅)
36::	⊢ (∃𝑦 ∈ 𝑏(𝑏 ∩ 𝑦) = ∅ ↔ ∃𝑦 (𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅))
37:36:	⊢ ∀𝑏(∃𝑦 ∈ 𝑏(𝑏 ∩ 𝑦) = ∅ ↔ ∃𝑦(𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅))
38:2,37:	⊢ ([(𝑎 ∩ 𝑥) / 𝑏]∃𝑦 ∈ 𝑏(𝑏 ∩ 𝑦) = ∅ ↔ [(𝑎 ∩ 𝑥) / 𝑏]∃𝑦(𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅))
39:35,38:	⊢ ([(𝑎 ∩ 𝑥) / 𝑏]∃𝑦 ∈ 𝑏(𝑏 ∩ 𝑦) = ∅ ↔ ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)
40:16,39:	⊢ (([(𝑎 ∩ 𝑥) / 𝑏](𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → [(𝑎 ∩ 𝑥) / 𝑏]∃𝑦 ∈ 𝑏(𝑏 ∩ 𝑦) = ∅) ↔ (((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅) → ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))
41:2:	⊢ ([(𝑎 ∩ 𝑥) / 𝑏]((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏(𝑏 ∩ 𝑦) = ∅) ↔ ([(𝑎 ∩ 𝑥) / 𝑏](𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → [(𝑎 ∩ 𝑥) / 𝑏]∃𝑦 ∈ 𝑏(𝑏 ∩ 𝑦) = ∅))
qed:40,41:	⊢ ([(𝑎 ∩ 𝑥) / 𝑏]((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏(𝑏 ∩ 𝑦) = ∅) ↔ (((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅) → ∃𝑦 ∈ (𝑎 ∩ 𝑥 )((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))

(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
onfrALTlem5VD	⊢ ([(𝑎 ∩ 𝑥) / 𝑏]((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅) ↔ (((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅) → ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))

Distinct variable groups:   𝑎,𝑏,𝑦   𝑥,𝑏,𝑦

Proof of Theorem onfrALTlem5VD

Step	Hyp	Ref	Expression
1		vex 3444	. . . 4 ⊢ 𝑎 ∈ V
2	1	inex1 5185	. . 3 ⊢ (𝑎 ∩ 𝑥) ∈ V
3		sbcimg 3767	. . 3 ⊢ ((𝑎 ∩ 𝑥) ∈ V → ([(𝑎 ∩ 𝑥) / 𝑏]((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅) ↔ ([(𝑎 ∩ 𝑥) / 𝑏](𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → [(𝑎 ∩ 𝑥) / 𝑏]∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅)))
4	2, 3	e0a 41478	. 2 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏]((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅) ↔ ([(𝑎 ∩ 𝑥) / 𝑏](𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → [(𝑎 ∩ 𝑥) / 𝑏]∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅))
5		sbcan 3768	. . . 4 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏](𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) ↔ ([(𝑎 ∩ 𝑥) / 𝑏]𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ [(𝑎 ∩ 𝑥) / 𝑏]𝑏 ≠ ∅))
6		sseq1 3940	. . . . . 6 ⊢ (𝑏 = (𝑎 ∩ 𝑥) → (𝑏 ⊆ (𝑎 ∩ 𝑥) ↔ (𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥)))
7	2, 6	sbcie 3760	. . . . 5 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏]𝑏 ⊆ (𝑎 ∩ 𝑥) ↔ (𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥))
8		df-ne 2988	. . . . . . 7 ⊢ (𝑏 ≠ ∅ ↔ ¬ 𝑏 = ∅)
9	8	sbcbii 3776	. . . . . 6 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏]𝑏 ≠ ∅ ↔ [(𝑎 ∩ 𝑥) / 𝑏] ¬ 𝑏 = ∅)
10		sbcng 3766	. . . . . . . 8 ⊢ ((𝑎 ∩ 𝑥) ∈ V → ([(𝑎 ∩ 𝑥) / 𝑏] ¬ 𝑏 = ∅ ↔ ¬ [(𝑎 ∩ 𝑥) / 𝑏]𝑏 = ∅))
11	10	bicomd 226	. . . . . . 7 ⊢ ((𝑎 ∩ 𝑥) ∈ V → (¬ [(𝑎 ∩ 𝑥) / 𝑏]𝑏 = ∅ ↔ [(𝑎 ∩ 𝑥) / 𝑏] ¬ 𝑏 = ∅))
12	2, 11	e0a 41478	. . . . . 6 ⊢ (¬ [(𝑎 ∩ 𝑥) / 𝑏]𝑏 = ∅ ↔ [(𝑎 ∩ 𝑥) / 𝑏] ¬ 𝑏 = ∅)
13		eqsbc3 3765	. . . . . . . 8 ⊢ ((𝑎 ∩ 𝑥) ∈ V → ([(𝑎 ∩ 𝑥) / 𝑏]𝑏 = ∅ ↔ (𝑎 ∩ 𝑥) = ∅))
14	2, 13	e0a 41478	. . . . . . 7 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏]𝑏 = ∅ ↔ (𝑎 ∩ 𝑥) = ∅)
15	14	necon3bbii 3034	. . . . . 6 ⊢ (¬ [(𝑎 ∩ 𝑥) / 𝑏]𝑏 = ∅ ↔ (𝑎 ∩ 𝑥) ≠ ∅)
16	9, 12, 15	3bitr2i 302	. . . . 5 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏]𝑏 ≠ ∅ ↔ (𝑎 ∩ 𝑥) ≠ ∅)
17	7, 16	anbi12i 629	. . . 4 ⊢ (([(𝑎 ∩ 𝑥) / 𝑏]𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ [(𝑎 ∩ 𝑥) / 𝑏]𝑏 ≠ ∅) ↔ ((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅))
18	5, 17	bitri 278	. . 3 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏](𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) ↔ ((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅))
19		df-rex 3112	. . . . 5 ⊢ (∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅ ↔ ∃𝑦(𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅))
20	19	sbcbii 3776	. . . 4 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏]∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅ ↔ [(𝑎 ∩ 𝑥) / 𝑏]∃𝑦(𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅))
21		sbcan 3768	. . . . . . 7 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏](𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅) ↔ ([(𝑎 ∩ 𝑥) / 𝑏]𝑦 ∈ 𝑏 ∧ [(𝑎 ∩ 𝑥) / 𝑏](𝑏 ∩ 𝑦) = ∅))
22		sbcel2gv 3787	. . . . . . . . 9 ⊢ ((𝑎 ∩ 𝑥) ∈ V → ([(𝑎 ∩ 𝑥) / 𝑏]𝑦 ∈ 𝑏 ↔ 𝑦 ∈ (𝑎 ∩ 𝑥)))
23	2, 22	e0a 41478	. . . . . . . 8 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏]𝑦 ∈ 𝑏 ↔ 𝑦 ∈ (𝑎 ∩ 𝑥))
24		sbceqg 4317	. . . . . . . . . 10 ⊢ ((𝑎 ∩ 𝑥) ∈ V → ([(𝑎 ∩ 𝑥) / 𝑏](𝑏 ∩ 𝑦) = ∅ ↔ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌(𝑏 ∩ 𝑦) = ⦋(𝑎 ∩ 𝑥) / 𝑏⦌∅))
25	2, 24	e0a 41478	. . . . . . . . 9 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏](𝑏 ∩ 𝑦) = ∅ ↔ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌(𝑏 ∩ 𝑦) = ⦋(𝑎 ∩ 𝑥) / 𝑏⦌∅)
26		csbin 4347	. . . . . . . . . . 11 ⊢ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌(𝑏 ∩ 𝑦) = (⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑏 ∩ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑦)
27		csbvarg 4339	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∩ 𝑥) ∈ V → ⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑏 = (𝑎 ∩ 𝑥))
28	2, 27	e0a 41478	. . . . . . . . . . . 12 ⊢ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑏 = (𝑎 ∩ 𝑥)
29		csbconstg 3847	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∩ 𝑥) ∈ V → ⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑦 = 𝑦)
30	2, 29	e0a 41478	. . . . . . . . . . . 12 ⊢ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑦 = 𝑦
31	28, 30	ineq12i 4137	. . . . . . . . . . 11 ⊢ (⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑏 ∩ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑦) = ((𝑎 ∩ 𝑥) ∩ 𝑦)
32	26, 31	eqtri 2821	. . . . . . . . . 10 ⊢ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌(𝑏 ∩ 𝑦) = ((𝑎 ∩ 𝑥) ∩ 𝑦)
33		csb0 4314	. . . . . . . . . 10 ⊢ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌∅ = ∅
34	32, 33	eqeq12i 2813	. . . . . . . . 9 ⊢ (⦋(𝑎 ∩ 𝑥) / 𝑏⦌(𝑏 ∩ 𝑦) = ⦋(𝑎 ∩ 𝑥) / 𝑏⦌∅ ↔ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)
35	25, 34	bitri 278	. . . . . . . 8 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏](𝑏 ∩ 𝑦) = ∅ ↔ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)
36	23, 35	anbi12i 629	. . . . . . 7 ⊢ (([(𝑎 ∩ 𝑥) / 𝑏]𝑦 ∈ 𝑏 ∧ [(𝑎 ∩ 𝑥) / 𝑏](𝑏 ∩ 𝑦) = ∅) ↔ (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))
37	21, 36	bitri 278	. . . . . 6 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏](𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅) ↔ (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))
38	37	exbii 1849	. . . . 5 ⊢ (∃𝑦[(𝑎 ∩ 𝑥) / 𝑏](𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅) ↔ ∃𝑦(𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))
39		sbcex2 3781	. . . . 5 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏]∃𝑦(𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅) ↔ ∃𝑦[(𝑎 ∩ 𝑥) / 𝑏](𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅))
40		df-rex 3112	. . . . 5 ⊢ (∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅ ↔ ∃𝑦(𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))
41	38, 39, 40	3bitr4i 306	. . . 4 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏]∃𝑦(𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅) ↔ ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)
42	20, 41	bitri 278	. . 3 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏]∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅ ↔ ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)
43	18, 42	imbi12i 354	. 2 ⊢ (([(𝑎 ∩ 𝑥) / 𝑏](𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → [(𝑎 ∩ 𝑥) / 𝑏]∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅) ↔ (((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅) → ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))
44	4, 43	bitri 278	1 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏]((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅) ↔ (((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅) → ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111   ≠ wne 2987  ∃wrex 3107  Vcvv 3441  [wsbc 3720  ⦋csb 3828   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-in 3888  df-ss 3898  df-nul 4244

This theorem is referenced by: (None)