Theorem dfdfat2 38778

Description: Alternate definition of the predicate "defined at" not using the Fun predicate. (Contributed by Alexander van der Vekens, 22-Jul-2017.)

Assertion

Ref	Expression
dfdfat2	|- ( F defAt A <-> ( A e. dom F /\ E! y A F y ) )

Distinct variable groups:   y, A   y, F

Proof of Theorem dfdfat2

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-dfat 38762	. 2 |- ( F defAt A <-> ( A e. dom F /\ Fun ( F |` { A } ) ) )
2		relres 5138	. . . 4 |- Rel ( F |` { A } )
3		dffun8 5616	. . . 4 |- ( Fun ( F |` { A } ) <-> ( Rel ( F |` { A } ) /\ A. x e. dom ( F |` { A } ) E! y x ( F |` { A } ) y ) )
4	2, 3	mpbiran 932	. . 3 |- ( Fun ( F |` { A } ) <-> A. x e. dom ( F |` { A } ) E! y x ( F |` { A } ) y )
5	4	anbi2i 708	. 2 |- ( ( A e. dom F /\ Fun ( F |` { A } ) ) <-> ( A e. dom F /\ A. x e. dom ( F |` { A } ) E! y x ( F |` { A } ) y ) )
6		vex 3034	. . . . . . . 8 |- y e. _V
7	6	brres 5117	. . . . . . 7 |- ( x ( F |` { A } ) y <-> ( x F y /\ x e. { A } ) )
8	7	a1i 11	. . . . . 6 |- ( A e. dom F -> ( x ( F |` { A } ) y <-> ( x F y /\ x e. { A } ) ) )
9	8	eubidv 2339	. . . . 5 |- ( A e. dom F -> ( E! y x ( F |` { A } ) y <-> E! y ( x F y /\ x e. { A } ) ) )
10	9	ralbidv 2829	. . . 4 |- ( A e. dom F -> ( A. x e. dom ( F |` { A } ) E! y x ( F |` { A } ) y <-> A. x e. dom ( F |` { A } ) E! y ( x F y /\ x e. { A } ) ) )
11		eldmressnsn 5150	. . . . 5 |- ( A e. dom F -> A e. dom ( F |` { A } ) )
12		eldmressn 38769	. . . . 5 |- ( x e. dom ( F |` { A } ) -> x = A )
13		breq1 4398	. . . . . . . 8 |- ( x = A -> ( x F y <-> A F y ) )
14	13	anbi1d 719	. . . . . . 7 |- ( x = A -> ( ( x F y /\ x e. { A } ) <-> ( A F y /\ x e. { A } ) ) )
15		elsn 3973	. . . . . . . . 9 |- ( x e. { A } <-> x = A )
16	15	biimpri 211	. . . . . . . 8 |- ( x = A -> x e. { A } )
17	16	biantrud 515	. . . . . . 7 |- ( x = A -> ( A F y <-> ( A F y /\ x e. { A } ) ) )
18	14, 17	bitr4d 264	. . . . . 6 |- ( x = A -> ( ( x F y /\ x e. { A } ) <-> A F y ) )
19	18	eubidv 2339	. . . . 5 |- ( x = A -> ( E! y ( x F y /\ x e. { A } ) <-> E! y A F y ) )
20	11, 12, 19	ralbinrald 38765	. . . 4 |- ( A e. dom F -> ( A. x e. dom ( F |` { A } ) E! y ( x F y /\ x e. { A } ) <-> E! y A F y ) )
21	10, 20	bitrd 261	. . 3 |- ( A e. dom F -> ( A. x e. dom ( F |` { A } ) E! y x ( F |` { A } ) y <-> E! y A F y ) )
22	21	pm5.32i 649	. 2 |- ( ( A e. dom F /\ A. x e. dom ( F |` { A } ) E! y x ( F |` { A } ) y ) <-> ( A e. dom F /\ E! y A F y ) )
23	1, 5, 22	3bitri 279	1 |- ( F defAt A <-> ( A e. dom F /\ E! y A F y ) )

Syntax hints:   <-> wb 189   /\ wa 376   = wceq 1452   e. wcel 1904   E!weu 2319   A.wral 2756   {csn 3959   class class class wbr 4395   dom cdm 4839   |` cres 4841   Rel wrel 4844   Fun wfun 5583   defAt wdfat 38759

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pr 4639

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-br 4396  df-opab 4455  df-id 4754  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-res 4851  df-fun 5591  df-dfat 38762

This theorem is referenced by:  afveu  38800  rlimdmafv  38824