Theorem onfrALTlem4VD 44390

Description: Virtual deduction proof of onfrALTlem4 44047. 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. onfrALTlem4 44047 is onfrALTlem4VD 44390 without virtual deductions and was automatically derived from onfrALTlem4VD 44390.

1::	⊢ 𝑦 ∈ V
2:1:	⊢ ([𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅ ↔ ⦋ 𝑦 / 𝑥⦌(𝑎 ∩ 𝑥) = ⦋𝑦 / 𝑥⦌∅)
3:1:	⊢ ⦋𝑦 / 𝑥⦌(𝑎 ∩ 𝑥) = (⦋𝑦 / 𝑥⦌ 𝑎 ∩ ⦋𝑦 / 𝑥⦌𝑥)
4:1:	⊢ ⦋𝑦 / 𝑥⦌𝑎 = 𝑎
5:1:	⊢ ⦋𝑦 / 𝑥⦌𝑥 = 𝑦
6:4,5:	⊢ (⦋𝑦 / 𝑥⦌𝑎 ∩ ⦋𝑦 / 𝑥⦌𝑥) = ( 𝑎 ∩ 𝑦)
7:3,6:	⊢ ⦋𝑦 / 𝑥⦌(𝑎 ∩ 𝑥) = (𝑎 ∩ 𝑦)
8:1:	⊢ ⦋𝑦 / 𝑥⦌∅ = ∅
9:7,8:	⊢ (⦋𝑦 / 𝑥⦌(𝑎 ∩ 𝑥) = ⦋𝑦 / 𝑥⦌ ∅ ↔ (𝑎 ∩ 𝑦) = ∅)
10:2,9:	⊢ ([𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅ ↔ (𝑎 ∩ 𝑦) = ∅)
11:1:	⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝑎 ↔ 𝑦 ∈ 𝑎)
12:11,10:	⊢ (([𝑦 / 𝑥]𝑥 ∈ 𝑎 ∧ [𝑦 / 𝑥]( 𝑎 ∩ 𝑥) = ∅) ↔ (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))
13:1:	⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ ([𝑦 / 𝑥]𝑥 ∈ 𝑎 ∧ [𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅))
qed:13,12:	⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))

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

Assertion

Ref	Expression
onfrALTlem4VD	⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))

Distinct variable group:   𝑥,𝑎

Proof of Theorem onfrALTlem4VD

Step	Hyp	Ref	Expression
1		sbcan 3827	. 2 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ ([𝑦 / 𝑥]𝑥 ∈ 𝑎 ∧ [𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅))
2		sbcel1v 3845	. . 3 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝑎 ↔ 𝑦 ∈ 𝑎)
3		sbceqg 4410	. . . . 5 ⊢ (𝑦 ∈ V → ([𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅ ↔ ⦋𝑦 / 𝑥⦌(𝑎 ∩ 𝑥) = ⦋𝑦 / 𝑥⦌∅))
4	3	elv 3469	. . . 4 ⊢ ([𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅ ↔ ⦋𝑦 / 𝑥⦌(𝑎 ∩ 𝑥) = ⦋𝑦 / 𝑥⦌∅)
5		csbin 4440	. . . . . 6 ⊢ ⦋𝑦 / 𝑥⦌(𝑎 ∩ 𝑥) = (⦋𝑦 / 𝑥⦌𝑎 ∩ ⦋𝑦 / 𝑥⦌𝑥)
6		csbconstg 3909	. . . . . . . 8 ⊢ (𝑦 ∈ V → ⦋𝑦 / 𝑥⦌𝑎 = 𝑎)
7	6	elv 3469	. . . . . . 7 ⊢ ⦋𝑦 / 𝑥⦌𝑎 = 𝑎
8		vex 3467	. . . . . . . 8 ⊢ 𝑦 ∈ V
9	8	csbvargi 4433	. . . . . . 7 ⊢ ⦋𝑦 / 𝑥⦌𝑥 = 𝑦
10	7, 9	ineq12i 4209	. . . . . 6 ⊢ (⦋𝑦 / 𝑥⦌𝑎 ∩ ⦋𝑦 / 𝑥⦌𝑥) = (𝑎 ∩ 𝑦)
11	5, 10	eqtri 2753	. . . . 5 ⊢ ⦋𝑦 / 𝑥⦌(𝑎 ∩ 𝑥) = (𝑎 ∩ 𝑦)
12		csb0 4408	. . . . 5 ⊢ ⦋𝑦 / 𝑥⦌∅ = ∅
13	11, 12	eqeq12i 2743	. . . 4 ⊢ (⦋𝑦 / 𝑥⦌(𝑎 ∩ 𝑥) = ⦋𝑦 / 𝑥⦌∅ ↔ (𝑎 ∩ 𝑦) = ∅)
14	4, 13	bitri 274	. . 3 ⊢ ([𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅ ↔ (𝑎 ∩ 𝑦) = ∅)
15	2, 14	anbi12i 626	. 2 ⊢ (([𝑦 / 𝑥]𝑥 ∈ 𝑎 ∧ [𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅) ↔ (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))
16	1, 15	bitri 274	1 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))

Syntax hints:   ↔ wb 205   ∧ wa 394   = wceq 1533  Vcvv 3463  [wsbc 3774  ⦋csb 3890   ∩ cin 3944  ∅c0 4323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-rab 3420  df-v 3465  df-sbc 3775  df-csb 3891  df-dif 3948  df-in 3952  df-nul 4324

This theorem is referenced by: (None)