Theorem onfrALTlem5VD 44905

Description: Virtual deduction proof of onfrALTlem5 44562. 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 44562 is onfrALTlem5VD 44905 without virtual deductions and was automatically derived from onfrALTlem5VD 44905.

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 3484	. . . 4 ⊢ 𝑎 ∈ V
2	1	inex1 5317	. . 3 ⊢ (𝑎 ∩ 𝑥) ∈ V
3		sbcimg 3837	. . 3 ⊢ ((𝑎 ∩ 𝑥) ∈ V → ([(𝑎 ∩ 𝑥) / 𝑏]((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅) ↔ ([(𝑎 ∩ 𝑥) / 𝑏](𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → [(𝑎 ∩ 𝑥) / 𝑏]∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅)))
4	2, 3	e0a 44792	. 2 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏]((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅) ↔ ([(𝑎 ∩ 𝑥) / 𝑏](𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → [(𝑎 ∩ 𝑥) / 𝑏]∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅))
5		sbcan 3838	. . . 4 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏](𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) ↔ ([(𝑎 ∩ 𝑥) / 𝑏]𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ [(𝑎 ∩ 𝑥) / 𝑏]𝑏 ≠ ∅))
6		sseq1 4009	. . . . . 6 ⊢ (𝑏 = (𝑎 ∩ 𝑥) → (𝑏 ⊆ (𝑎 ∩ 𝑥) ↔ (𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥)))
7	2, 6	sbcie 3830	. . . . 5 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏]𝑏 ⊆ (𝑎 ∩ 𝑥) ↔ (𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥))
8		df-ne 2941	. . . . . . 7 ⊢ (𝑏 ≠ ∅ ↔ ¬ 𝑏 = ∅)
9	8	sbcbii 3846	. . . . . 6 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏]𝑏 ≠ ∅ ↔ [(𝑎 ∩ 𝑥) / 𝑏] ¬ 𝑏 = ∅)
10		sbcng 3836	. . . . . . . 8 ⊢ ((𝑎 ∩ 𝑥) ∈ V → ([(𝑎 ∩ 𝑥) / 𝑏] ¬ 𝑏 = ∅ ↔ ¬ [(𝑎 ∩ 𝑥) / 𝑏]𝑏 = ∅))
11	10	bicomd 223	. . . . . . 7 ⊢ ((𝑎 ∩ 𝑥) ∈ V → (¬ [(𝑎 ∩ 𝑥) / 𝑏]𝑏 = ∅ ↔ [(𝑎 ∩ 𝑥) / 𝑏] ¬ 𝑏 = ∅))
12	2, 11	e0a 44792	. . . . . 6 ⊢ (¬ [(𝑎 ∩ 𝑥) / 𝑏]𝑏 = ∅ ↔ [(𝑎 ∩ 𝑥) / 𝑏] ¬ 𝑏 = ∅)
13		eqsbc1 3835	. . . . . . . 8 ⊢ ((𝑎 ∩ 𝑥) ∈ V → ([(𝑎 ∩ 𝑥) / 𝑏]𝑏 = ∅ ↔ (𝑎 ∩ 𝑥) = ∅))
14	2, 13	e0a 44792	. . . . . . 7 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏]𝑏 = ∅ ↔ (𝑎 ∩ 𝑥) = ∅)
15	14	necon3bbii 2988	. . . . . 6 ⊢ (¬ [(𝑎 ∩ 𝑥) / 𝑏]𝑏 = ∅ ↔ (𝑎 ∩ 𝑥) ≠ ∅)
16	9, 12, 15	3bitr2i 299	. . . . 5 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏]𝑏 ≠ ∅ ↔ (𝑎 ∩ 𝑥) ≠ ∅)
17	7, 16	anbi12i 628	. . . 4 ⊢ (([(𝑎 ∩ 𝑥) / 𝑏]𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ [(𝑎 ∩ 𝑥) / 𝑏]𝑏 ≠ ∅) ↔ ((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅))
18	5, 17	bitri 275	. . 3 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏](𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) ↔ ((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅))
19		df-rex 3071	. . . . 5 ⊢ (∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅ ↔ ∃𝑦(𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅))
20	19	sbcbii 3846	. . . 4 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏]∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅ ↔ [(𝑎 ∩ 𝑥) / 𝑏]∃𝑦(𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅))
21		sbcan 3838	. . . . . . 7 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏](𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅) ↔ ([(𝑎 ∩ 𝑥) / 𝑏]𝑦 ∈ 𝑏 ∧ [(𝑎 ∩ 𝑥) / 𝑏](𝑏 ∩ 𝑦) = ∅))
22		sbcel2gv 3857	. . . . . . . . 9 ⊢ ((𝑎 ∩ 𝑥) ∈ V → ([(𝑎 ∩ 𝑥) / 𝑏]𝑦 ∈ 𝑏 ↔ 𝑦 ∈ (𝑎 ∩ 𝑥)))
23	2, 22	e0a 44792	. . . . . . . 8 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏]𝑦 ∈ 𝑏 ↔ 𝑦 ∈ (𝑎 ∩ 𝑥))
24		sbceqg 4412	. . . . . . . . . 10 ⊢ ((𝑎 ∩ 𝑥) ∈ V → ([(𝑎 ∩ 𝑥) / 𝑏](𝑏 ∩ 𝑦) = ∅ ↔ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌(𝑏 ∩ 𝑦) = ⦋(𝑎 ∩ 𝑥) / 𝑏⦌∅))
25	2, 24	e0a 44792	. . . . . . . . 9 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏](𝑏 ∩ 𝑦) = ∅ ↔ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌(𝑏 ∩ 𝑦) = ⦋(𝑎 ∩ 𝑥) / 𝑏⦌∅)
26		csbin 4442	. . . . . . . . . . 11 ⊢ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌(𝑏 ∩ 𝑦) = (⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑏 ∩ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑦)
27		csbvarg 4434	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∩ 𝑥) ∈ V → ⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑏 = (𝑎 ∩ 𝑥))
28	2, 27	e0a 44792	. . . . . . . . . . . 12 ⊢ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑏 = (𝑎 ∩ 𝑥)
29		csbconstg 3918	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∩ 𝑥) ∈ V → ⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑦 = 𝑦)
30	2, 29	e0a 44792	. . . . . . . . . . . 12 ⊢ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑦 = 𝑦
31	28, 30	ineq12i 4218	. . . . . . . . . . 11 ⊢ (⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑏 ∩ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑦) = ((𝑎 ∩ 𝑥) ∩ 𝑦)
32	26, 31	eqtri 2765	. . . . . . . . . 10 ⊢ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌(𝑏 ∩ 𝑦) = ((𝑎 ∩ 𝑥) ∩ 𝑦)
33		csb0 4410	. . . . . . . . . 10 ⊢ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌∅ = ∅
34	32, 33	eqeq12i 2755	. . . . . . . . 9 ⊢ (⦋(𝑎 ∩ 𝑥) / 𝑏⦌(𝑏 ∩ 𝑦) = ⦋(𝑎 ∩ 𝑥) / 𝑏⦌∅ ↔ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)
35	25, 34	bitri 275	. . . . . . . 8 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏](𝑏 ∩ 𝑦) = ∅ ↔ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)
36	23, 35	anbi12i 628	. . . . . . 7 ⊢ (([(𝑎 ∩ 𝑥) / 𝑏]𝑦 ∈ 𝑏 ∧ [(𝑎 ∩ 𝑥) / 𝑏](𝑏 ∩ 𝑦) = ∅) ↔ (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))
37	21, 36	bitri 275	. . . . . 6 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏](𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅) ↔ (𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))
38	37	exbii 1848	. . . . 5 ⊢ (∃𝑦[(𝑎 ∩ 𝑥) / 𝑏](𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅) ↔ ∃𝑦(𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))
39		sbcex2 3850	. . . . 5 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏]∃𝑦(𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅) ↔ ∃𝑦[(𝑎 ∩ 𝑥) / 𝑏](𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅))
40		df-rex 3071	. . . . 5 ⊢ (∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅ ↔ ∃𝑦(𝑦 ∈ (𝑎 ∩ 𝑥) ∧ ((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))
41	38, 39, 40	3bitr4i 303	. . . 4 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏]∃𝑦(𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅) ↔ ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)
42	20, 41	bitri 275	. . 3 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏]∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅ ↔ ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅)
43	18, 42	imbi12i 350	. 2 ⊢ (([(𝑎 ∩ 𝑥) / 𝑏](𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → [(𝑎 ∩ 𝑥) / 𝑏]∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅) ↔ (((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅) → ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))
44	4, 43	bitri 275	1 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏]((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅) ↔ (((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅) → ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2108   ≠ wne 2940  ∃wrex 3070  Vcvv 3480  [wsbc 3788  ⦋csb 3899   ∩ cin 3950   ⊆ wss 3951  ∅c0 4333

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-in 3958  df-ss 3968  df-nul 4334

This theorem is referenced by: (None)