Theorem onfrALTlem5VD 44861

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

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 3442	. . . 4 ⊢ 𝑎 ∈ V
2	1	inex1 5259	. . 3 ⊢ (𝑎 ∩ 𝑥) ∈ V
3		sbcimg 3793	. . 3 ⊢ ((𝑎 ∩ 𝑥) ∈ V → ([(𝑎 ∩ 𝑥) / 𝑏]((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅) ↔ ([(𝑎 ∩ 𝑥) / 𝑏](𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → [(𝑎 ∩ 𝑥) / 𝑏]∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅)))
4	2, 3	e0a 44748	. 2 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏]((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅) ↔ ([(𝑎 ∩ 𝑥) / 𝑏](𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → [(𝑎 ∩ 𝑥) / 𝑏]∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅))
5		sbcan 3794	. . . 4 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏](𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) ↔ ([(𝑎 ∩ 𝑥) / 𝑏]𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ [(𝑎 ∩ 𝑥) / 𝑏]𝑏 ≠ ∅))
6		sseq1 3963	. . . . . 6 ⊢ (𝑏 = (𝑎 ∩ 𝑥) → (𝑏 ⊆ (𝑎 ∩ 𝑥) ↔ (𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥)))
7	2, 6	sbcie 3786	. . . . 5 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏]𝑏 ⊆ (𝑎 ∩ 𝑥) ↔ (𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥))
8		df-ne 2926	. . . . . . 7 ⊢ (𝑏 ≠ ∅ ↔ ¬ 𝑏 = ∅)
9	8	sbcbii 3801	. . . . . 6 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏]𝑏 ≠ ∅ ↔ [(𝑎 ∩ 𝑥) / 𝑏] ¬ 𝑏 = ∅)
10		sbcng 3792	. . . . . . . 8 ⊢ ((𝑎 ∩ 𝑥) ∈ V → ([(𝑎 ∩ 𝑥) / 𝑏] ¬ 𝑏 = ∅ ↔ ¬ [(𝑎 ∩ 𝑥) / 𝑏]𝑏 = ∅))
11	10	bicomd 223	. . . . . . 7 ⊢ ((𝑎 ∩ 𝑥) ∈ V → (¬ [(𝑎 ∩ 𝑥) / 𝑏]𝑏 = ∅ ↔ [(𝑎 ∩ 𝑥) / 𝑏] ¬ 𝑏 = ∅))
12	2, 11	e0a 44748	. . . . . 6 ⊢ (¬ [(𝑎 ∩ 𝑥) / 𝑏]𝑏 = ∅ ↔ [(𝑎 ∩ 𝑥) / 𝑏] ¬ 𝑏 = ∅)
13		eqsbc1 3791	. . . . . . . 8 ⊢ ((𝑎 ∩ 𝑥) ∈ V → ([(𝑎 ∩ 𝑥) / 𝑏]𝑏 = ∅ ↔ (𝑎 ∩ 𝑥) = ∅))
14	2, 13	e0a 44748	. . . . . . 7 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏]𝑏 = ∅ ↔ (𝑎 ∩ 𝑥) = ∅)
15	14	necon3bbii 2972	. . . . . 6 ⊢ (¬ [(𝑎 ∩ 𝑥) / 𝑏]𝑏 = ∅ ↔ (𝑎 ∩ 𝑥) ≠ ∅)
16	9, 12, 15	3bitr2i 299	. . . . 5 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏]𝑏 ≠ ∅ ↔ (𝑎 ∩ 𝑥) ≠ ∅)
17	7, 16	anbi12i 628	. . . 4 ⊢ (([(𝑎 ∩ 𝑥) / 𝑏]𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ [(𝑎 ∩ 𝑥) / 𝑏]𝑏 ≠ ∅) ↔ ((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅))
18	5, 17	bitri 275	. . 3 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏](𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) ↔ ((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅))
19		df-rex 3054	. . . . 5 ⊢ (∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅ ↔ ∃𝑦(𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅))
20	19	sbcbii 3801	. . . 4 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏]∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅ ↔ [(𝑎 ∩ 𝑥) / 𝑏]∃𝑦(𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅))
21		sbcan 3794	. . . . . . 7 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏](𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅) ↔ ([(𝑎 ∩ 𝑥) / 𝑏]𝑦 ∈ 𝑏 ∧ [(𝑎 ∩ 𝑥) / 𝑏](𝑏 ∩ 𝑦) = ∅))
22		sbcel2gv 3811	. . . . . . . . 9 ⊢ ((𝑎 ∩ 𝑥) ∈ V → ([(𝑎 ∩ 𝑥) / 𝑏]𝑦 ∈ 𝑏 ↔ 𝑦 ∈ (𝑎 ∩ 𝑥)))
23	2, 22	e0a 44748	. . . . . . . 8 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏]𝑦 ∈ 𝑏 ↔ 𝑦 ∈ (𝑎 ∩ 𝑥))
24		sbceqg 4365	. . . . . . . . . 10 ⊢ ((𝑎 ∩ 𝑥) ∈ V → ([(𝑎 ∩ 𝑥) / 𝑏](𝑏 ∩ 𝑦) = ∅ ↔ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌(𝑏 ∩ 𝑦) = ⦋(𝑎 ∩ 𝑥) / 𝑏⦌∅))
25	2, 24	e0a 44748	. . . . . . . . 9 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏](𝑏 ∩ 𝑦) = ∅ ↔ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌(𝑏 ∩ 𝑦) = ⦋(𝑎 ∩ 𝑥) / 𝑏⦌∅)
26		csbin 4395	. . . . . . . . . . 11 ⊢ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌(𝑏 ∩ 𝑦) = (⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑏 ∩ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑦)
27		csbvarg 4387	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∩ 𝑥) ∈ V → ⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑏 = (𝑎 ∩ 𝑥))
28	2, 27	e0a 44748	. . . . . . . . . . . 12 ⊢ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑏 = (𝑎 ∩ 𝑥)
29		csbconstg 3872	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∩ 𝑥) ∈ V → ⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑦 = 𝑦)
30	2, 29	e0a 44748	. . . . . . . . . . . 12 ⊢ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑦 = 𝑦
31	28, 30	ineq12i 4171	. . . . . . . . . . 11 ⊢ (⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑏 ∩ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌𝑦) = ((𝑎 ∩ 𝑥) ∩ 𝑦)
32	26, 31	eqtri 2752	. . . . . . . . . 10 ⊢ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌(𝑏 ∩ 𝑦) = ((𝑎 ∩ 𝑥) ∩ 𝑦)
33		csb0 4363	. . . . . . . . . 10 ⊢ ⦋(𝑎 ∩ 𝑥) / 𝑏⦌∅ = ∅
34	32, 33	eqeq12i 2747	. . . . . . . . 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 3805	. . . . 5 ⊢ ([(𝑎 ∩ 𝑥) / 𝑏]∃𝑦(𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅) ↔ ∃𝑦[(𝑎 ∩ 𝑥) / 𝑏](𝑦 ∈ 𝑏 ∧ (𝑏 ∩ 𝑦) = ∅))
40		df-rex 3054	. . . . 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 2109   ≠ wne 2925  ∃wrex 3053  Vcvv 3438  [wsbc 3744  ⦋csb 3853   ∩ cin 3904   ⊆ wss 3905  ∅c0 4286

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-rex 3054  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-in 3912  df-ss 3922  df-nul 4287

This theorem is referenced by: (None)