Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > abbi2i | Structured version Visualization version Unicode version |
Description: Equality of a class variable and a class abstraction (inference rule). (Contributed by NM, 26-May-1993.) |
Ref | Expression |
---|---|
abbi2i.1 |
Ref | Expression |
---|---|
abbi2i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | abeq2 2732 | . 2 | |
2 | abbi2i.1 | . 2 | |
3 | 1, 2 | mpgbir 1726 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 196 wceq 1483 wcel 1990 cab 2608 |
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-11 2034 ax-12 2047 ax-13 2246 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 |
This theorem is referenced by: abid1 2744 cbvralcsf 3565 cbvreucsf 3567 cbvrabcsf 3568 dfsymdif2 3851 symdif2 3852 dfnul2 3917 dfpr2 4195 dftp2 4231 0iin 4578 pwpwab 4614 epse 5097 fv3 6206 fo1st 7188 fo2nd 7189 xp2 7203 tfrlem3 7474 mapsn 7899 ixpconstg 7917 ixp0x 7936 dfom4 8546 cardnum 8917 alephiso 8921 nnzrab 11405 nn0zrab 11406 qnnen 14942 h2hcau 27836 dfch2 28266 hhcno 28763 hhcnf 28764 pjhmopidm 29042 bdayfo 31828 madeval2 31936 fobigcup 32007 dfsingles2 32028 dfrecs2 32057 dfrdg4 32058 dfint3 32059 bj-snglinv 32960 ecres 34043 dfdm6 34071 compeq 38642 |
Copyright terms: Public domain | W3C validator |