Theorem csbrngVD 37160

Description: Virtual deduction proof of csbrngOLD 37084. 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. csbrngOLD 37084 is csbrngVD 37160 without virtual deductions and was automatically derived from csbrngVD 37160.

1::	|- (. A e. V ->. A e. V ).
2:1:	|- (. A e. V ->. ( [. A / x ]. <. w ,. y >. e. B <-> [_ A / x ]_ <. w , y >. e. [_ A / x ]_ B ) ).
3:1:	|- (. A e. V ->. [_ A / x ]_ <. w ,. y >. = <. w , y >. ).
4:3:	|- (. A e. V ->. ( [_ A / x ]_ <. w ,. y >. e. [_ A / x ]_ B <-> <. w , y >. e. [_ A / x ]_ B ) ).
5:2,4:	|- (. A e. V ->. ( [. A / x ]. <. w ,. y >. e. B <-> <. w , y >. e. [_ A / x ]_ B ) ).
6:5:	|- (. A e. V ->. A. w ( [. A / x ]. <. w ,. y >. e. B <-> <. w , y >. e. [_ A / x ]_ B ) ).
7:6:	|- (. A e. V ->. ( E. w [. A / x ]. <. w ,. y >. e. B <-> E. w <. w , y >. e. [_ A / x ]_ B ) ).
8:1:	|- (. A e. V ->. ( E. w [. A / x ]. <. w ,. y >. e. B <-> [. A / x ]. E. w <. w , y >. e. B ) ).
9:7,8:	|- (. A e. V ->. ( [. A / x ]. E. w <. w ,. y >. e. B <-> E. w <. w , y >. e. [_ A / x ]_ B ) ).
10:9:	|- (. A e. V ->. A. y ( [. A / x ]. E. w <. w , y >. e. B <-> E. w <. w , y >. e. [_ A / x ]_ B ) ).
11:10:	|- (. A e. V ->. { y | [. A / x ]. E. w <. w , y >. e. B } = { y | E. w <. w , y >. e. [_ A / x ]_ B } ).
12:1:	|- (. A e. V ->. [_ A / x ]_ { y | E. w <. w , y >. e. B } = { y | [. A / x ]. E. w <. w , y >. e. B } ).
13:11,12:	|- (. A e. V ->. [_ A / x ]_ { y | E. w <. w , y >. e. B } = { y | E. w <. w , y >. e. [_ A / x ]_ B } ).
14::	|- ran B = { y | E. w <. w ,. y >. e. B }
15:14:	|- A. x ran B = { y | E. w <. w ,. y >. e. B }
16:1,15:	|- (. A e. V ->. [_ A / x ]_ ran B = [_ A / x ]_ { y | E. w <. w , y >. e. B } ).
17:13,16:	|- (. A e. V ->. [_ A / x ]_ ran B = { y | E. w <. w , y >. e. [_ A / x ]_ B } ).
18::	|- ran [_ A / x ]_ B = { y | E. w <. w ,. y >. e. [_ A / x ]_ B }
19:17,18:	|- (. A e. V ->. [_ A / x ]_ ran B = ran [_ A / x ]_ B ).
qed:19:	|- ( A e. V -> [_ A / x ]_ ran B = ran [_ A / x ]_ B )

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

Assertion

Ref	Expression
csbrngVD	|- ( A e. V -> [_ A / x ]_ ran B = ran [_ A / x ]_ B )

Proof of Theorem csbrngVD

Dummy variables w y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		idn1 36809	. . . . . . . . . . . 12 |- (. A e. V ->. A e. V ).
2		sbcel12gOLD 36769	. . . . . . . . . . . 12 |- ( A e. V -> ( [. A / x ]. <. w , y >. e. B <-> [_ A / x ]_ <. w , y >. e. [_ A / x ]_ B ) )
3	1, 2	e1a 36871	. . . . . . . . . . 11 |- (. A e. V ->. ( [. A / x ]. <. w , y >. e. B <-> [_ A / x ]_ <. w , y >. e. [_ A / x ]_ B ) ).
4		csbconstg 3409	. . . . . . . . . . . . 13 |- ( A e. V -> [_ A / x ]_ <. w , y >. = <. w , y >. )
5	1, 4	e1a 36871	. . . . . . . . . . . 12 |- (. A e. V ->. [_ A / x ]_ <. w , y >. = <. w , y >. ).
6		eleq1 2495	. . . . . . . . . . . 12 |- ( [_ A / x ]_ <. w , y >. = <. w , y >. -> ( [_ A / x ]_ <. w , y >. e. [_ A / x ]_ B <-> <. w , y >. e. [_ A / x ]_ B ) )
7	5, 6	e1a 36871	. . . . . . . . . . 11 |- (. A e. V ->. ( [_ A / x ]_ <. w , y >. e. [_ A / x ]_ B <-> <. w , y >. e. [_ A / x ]_ B ) ).
8		bibi1 329	. . . . . . . . . . . 12 |- ( ( [. A / x ]. <. w , y >. e. B <-> [_ A / x ]_ <. w , y >. e. [_ A / x ]_ B ) -> ( ( [. A / x ]. <. w , y >. e. B <-> <. w , y >. e. [_ A / x ]_ B ) <-> ( [_ A / x ]_ <. w , y >. e. [_ A / x ]_ B <-> <. w , y >. e. [_ A / x ]_ B ) ) )
9	8	biimprd 227	. . . . . . . . . . 11 |- ( ( [. A / x ]. <. w , y >. e. B <-> [_ A / x ]_ <. w , y >. e. [_ A / x ]_ B ) -> ( ( [_ A / x ]_ <. w , y >. e. [_ A / x ]_ B <-> <. w , y >. e. [_ A / x ]_ B ) -> ( [. A / x ]. <. w , y >. e. B <-> <. w , y >. e. [_ A / x ]_ B ) ) )
10	3, 7, 9	e11 36932	. . . . . . . . . 10 |- (. A e. V ->. ( [. A / x ]. <. w , y >. e. B <-> <. w , y >. e. [_ A / x ]_ B ) ).
11	10	gen11 36860	. . . . . . . . 9 |- (. A e. V ->. A. w ( [. A / x ]. <. w , y >. e. B <-> <. w , y >. e. [_ A / x ]_ B ) ).
12		exbi 1712	. . . . . . . . 9 |- ( A. w ( [. A / x ]. <. w , y >. e. B <-> <. w , y >. e. [_ A / x ]_ B ) -> ( E. w [. A / x ]. <. w , y >. e. B <-> E. w <. w , y >. e. [_ A / x ]_ B ) )
13	11, 12	e1a 36871	. . . . . . . 8 |- (. A e. V ->. ( E. w [. A / x ]. <. w , y >. e. B <-> E. w <. w , y >. e. [_ A / x ]_ B ) ).
14		sbcexgOLD 36768	. . . . . . . . . 10 |- ( A e. V -> ( [. A / x ]. E. w <. w , y >. e. B <-> E. w [. A / x ]. <. w , y >. e. B ) )
15	14	bicomd 205	. . . . . . . . 9 |- ( A e. V -> ( E. w [. A / x ]. <. w , y >. e. B <-> [. A / x ]. E. w <. w , y >. e. B ) )
16	1, 15	e1a 36871	. . . . . . . 8 |- (. A e. V ->. ( E. w [. A / x ]. <. w , y >. e. B <-> [. A / x ]. E. w <. w , y >. e. B ) ).
17		bitr3 36731	. . . . . . . . 9 |- ( ( E. w [. A / x ]. <. w , y >. e. B <-> [. A / x ]. E. w <. w , y >. e. B ) -> ( ( E. w [. A / x ]. <. w , y >. e. B <-> E. w <. w , y >. e. [_ A / x ]_ B ) -> ( [. A / x ]. E. w <. w , y >. e. B <-> E. w <. w , y >. e. [_ A / x ]_ B ) ) )
18	17	com12 33	. . . . . . . 8 |- ( ( E. w [. A / x ]. <. w , y >. e. B <-> E. w <. w , y >. e. [_ A / x ]_ B ) -> ( ( E. w [. A / x ]. <. w , y >. e. B <-> [. A / x ]. E. w <. w , y >. e. B ) -> ( [. A / x ]. E. w <. w , y >. e. B <-> E. w <. w , y >. e. [_ A / x ]_ B ) ) )
19	13, 16, 18	e11 36932	. . . . . . 7 |- (. A e. V ->. ( [. A / x ]. E. w <. w , y >. e. B <-> E. w <. w , y >. e. [_ A / x ]_ B ) ).
20	19	gen11 36860	. . . . . 6 |- (. A e. V ->. A. y ( [. A / x ]. E. w <. w , y >. e. B <-> E. w <. w , y >. e. [_ A / x ]_ B ) ).
21		abbi 2554	. . . . . . 7 |- ( A. y ( [. A / x ]. E. w <. w , y >. e. B <-> E. w <. w , y >. e. [_ A / x ]_ B ) <-> { y | [. A / x ]. E. w <. w , y >. e. B } = { y | E. w <. w , y >. e. [_ A / x ]_ B } )
22	21	biimpi 198	. . . . . 6 |- ( A. y ( [. A / x ]. E. w <. w , y >. e. B <-> E. w <. w , y >. e. [_ A / x ]_ B ) -> { y | [. A / x ]. E. w <. w , y >. e. B } = { y | E. w <. w , y >. e. [_ A / x ]_ B } )
23	20, 22	e1a 36871	. . . . 5 |- (. A e. V ->. { y | [. A / x ]. E. w <. w , y >. e. B } = { y | E. w <. w , y >. e. [_ A / x ]_ B } ).
24		csbabgOLD 37078	. . . . . 6 |- ( A e. V -> [_ A / x ]_ { y | E. w <. w , y >. e. B } = { y | [. A / x ]. E. w <. w , y >. e. B } )
25	1, 24	e1a 36871	. . . . 5 |- (. A e. V ->. [_ A / x ]_ { y | E. w <. w , y >. e. B } = { y | [. A / x ]. E. w <. w , y >. e. B } ).
26		eqeq2 2438	. . . . . 6 |- ( { y | [. A / x ]. E. w <. w , y >. e. B } = { y | E. w <. w , y >. e. [_ A / x ]_ B } -> ( [_ A / x ]_ { y | E. w <. w , y >. e. B } = { y | [. A / x ]. E. w <. w , y >. e. B } <-> [_ A / x ]_ { y | E. w <. w , y >. e. B } = { y | E. w <. w , y >. e. [_ A / x ]_ B } ) )
27	26	biimpd 211	. . . . 5 |- ( { y | [. A / x ]. E. w <. w , y >. e. B } = { y | E. w <. w , y >. e. [_ A / x ]_ B } -> ( [_ A / x ]_ { y | E. w <. w , y >. e. B } = { y | [. A / x ]. E. w <. w , y >. e. B } -> [_ A / x ]_ { y | E. w <. w , y >. e. B } = { y | E. w <. w , y >. e. [_ A / x ]_ B } ) )
28	23, 25, 27	e11 36932	. . . 4 |- (. A e. V ->. [_ A / x ]_ { y | E. w <. w , y >. e. B } = { y | E. w <. w , y >. e. [_ A / x ]_ B } ).
29		dfrn3 5041	. . . . . 6 |- ran B = { y | E. w <. w , y >. e. B }
30	29	ax-gen 1666	. . . . 5 |- A. x ran B = { y | E. w <. w , y >. e. B }
31		csbeq2gOLD 36780	. . . . 5 |- ( A e. V -> ( A. x ran B = { y | E. w <. w , y >. e. B } -> [_ A / x ]_ ran B = [_ A / x ]_ { y | E. w <. w , y >. e. B } ) )
32	1, 30, 31	e10 36938	. . . 4 |- (. A e. V ->. [_ A / x ]_ ran B = [_ A / x ]_ { y | E. w <. w , y >. e. B } ).
33		eqeq2 2438	. . . . 5 |- ( [_ A / x ]_ { y | E. w <. w , y >. e. B } = { y | E. w <. w , y >. e. [_ A / x ]_ B } -> ( [_ A / x ]_ ran B = [_ A / x ]_ { y | E. w <. w , y >. e. B } <-> [_ A / x ]_ ran B = { y | E. w <. w , y >. e. [_ A / x ]_ B } ) )
34	33	biimpd 211	. . . 4 |- ( [_ A / x ]_ { y | E. w <. w , y >. e. B } = { y | E. w <. w , y >. e. [_ A / x ]_ B } -> ( [_ A / x ]_ ran B = [_ A / x ]_ { y | E. w <. w , y >. e. B } -> [_ A / x ]_ ran B = { y | E. w <. w , y >. e. [_ A / x ]_ B } ) )
35	28, 32, 34	e11 36932	. . 3 |- (. A e. V ->. [_ A / x ]_ ran B = { y | E. w <. w , y >. e. [_ A / x ]_ B } ).
36		dfrn3 5041	. . 3 |- ran [_ A / x ]_ B = { y | E. w <. w , y >. e. [_ A / x ]_ B }
37		eqeq2 2438	. . . 4 |- ( ran [_ A / x ]_ B = { y | E. w <. w , y >. e. [_ A / x ]_ B } -> ( [_ A / x ]_ ran B = ran [_ A / x ]_ B <-> [_ A / x ]_ ran B = { y | E. w <. w , y >. e. [_ A / x ]_ B } ) )
38	37	biimprcd 229	. . 3 |- ( [_ A / x ]_ ran B = { y | E. w <. w , y >. e. [_ A / x ]_ B } -> ( ran [_ A / x ]_ B = { y | E. w <. w , y >. e. [_ A / x ]_ B } -> [_ A / x ]_ ran B = ran [_ A / x ]_ B ) )
39	35, 36, 38	e10 36938	. 2 |- (. A e. V ->. [_ A / x ]_ ran B = ran [_ A / x ]_ B ).
40	39	in1 36806	1 |- ( A e. V -> [_ A / x ]_ ran B = ran [_ A / x ]_ B )

Syntax hints:   -> wi 4   <-> wb 188   A.wal 1436   = wceq 1438   E.wex 1660   e. wcel 1869   {cab 2408   [.wsbc 3300   [_csb 3396   <.cop 4003   ran crn 4852

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pr 4658

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-rab 2785  df-v 3084  df-sbc 3301  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-sn 3998  df-pr 4000  df-op 4004  df-br 4422  df-opab 4481  df-cnv 4859  df-dm 4861  df-rn 4862  df-vd1 36805

This theorem is referenced by: (None)