| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > reqabi | Structured version Visualization version GIF version | ||
| Description: Inference from equality of a class variable and a restricted class abstraction. (Contributed by NM, 16-Feb-2004.) |
| Ref | Expression |
|---|---|
| reqabi.1 | ⊢ 𝐴 = {𝑥 ∈ 𝐵 ∣ 𝜑} |
| Ref | Expression |
|---|---|
| reqabi | ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ∧ 𝜑)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | reqabi.1 | . . 3 ⊢ 𝐴 = {𝑥 ∈ 𝐵 ∣ 𝜑} | |
| 2 | 1 | eleq2i 2833 | . 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑}) |
| 3 | rabid 3458 | . 2 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝑥 ∈ 𝐵 ∧ 𝜑)) | |
| 4 | 2, 3 | bitri 275 | 1 ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ∧ 𝜑)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2108 {crab 3436 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-12 2177 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 |
| This theorem is referenced by: fvmptss 7028 tfis 7876 nqereu 10969 rpnnen1lem2 13019 rpnnen1lem1 13020 rpnnen1lem3 13021 rpnnen1lem5 13023 qustgpopn 24128 addsproplem2 28003 sleadd1 28022 negsproplem6 28065 negsid 28073 nbusgrf1o0 29386 finsumvtxdg2ssteplem3 29565 frgrwopreglem2 30332 frgrwopreglem5lem 30339 resf1o 32741 elrgspnlem4 33249 nsgqusf1olem2 33442 nsgqusf1olem3 33443 ballotlem2 34491 reprsuc 34630 oddprm2 34670 hgt750lemb 34671 bnj1476 34861 bnj1533 34866 bnj1538 34869 bnj1523 35085 cvmlift2lem12 35319 neibastop2lem 36361 topdifinfindis 37347 topdifinffinlem 37348 stoweidlem24 46039 stoweidlem31 46046 stoweidlem52 46067 stoweidlem54 46069 stoweidlem57 46072 salexct 46349 ovolval5lem3 46669 pimdecfgtioc 46730 pimincfltioc 46731 pimdecfgtioo 46732 pimincfltioo 46733 smfsuplem1 46826 smfsuplem3 46828 smfliminflem 46845 prprsprreu 47506 |
| Copyright terms: Public domain | W3C validator |