Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ceqsrexv | Structured version Visualization version Unicode version |
Description: Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by NM, 30-Apr-2004.) |
Ref | Expression |
---|---|
ceqsrexv.1 |
Ref | Expression |
---|---|
ceqsrexv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rex 2918 | . . 3 | |
2 | an12 838 | . . . 4 | |
3 | 2 | exbii 1774 | . . 3 |
4 | 1, 3 | bitr4i 267 | . 2 |
5 | eleq1 2689 | . . . . 5 | |
6 | ceqsrexv.1 | . . . . 5 | |
7 | 5, 6 | anbi12d 747 | . . . 4 |
8 | 7 | ceqsexgv 3335 | . . 3 |
9 | 8 | bianabs 924 | . 2 |
10 | 4, 9 | syl5bb 272 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wa 384 wceq 1483 wex 1704 wcel 1990 wrex 2913 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-12 2047 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-rex 2918 df-v 3202 |
This theorem is referenced by: ceqsrexbv 3337 ceqsrex2v 3338 reuxfr2d 4891 f1oiso 6601 creur 11014 creui 11015 deg1ldg 23852 ulm2 24139 iscgra1 25702 reuxfr3d 29329 poimirlem24 33433 eqlkr3 34388 diclspsn 36483 rmxdiophlem 37582 expdiophlem1 37588 expdiophlem2 37589 |
Copyright terms: Public domain | W3C validator |