Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > elrabd | Structured version Visualization version GIF version |
Description: Membership in a restricted class abstraction, using implicit substitution. Deduction version of elrab 3677. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
Ref | Expression |
---|---|
elrabd.1 | ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒)) |
elrabd.2 | ⊢ (𝜑 → 𝐴 ∈ 𝐵) |
elrabd.3 | ⊢ (𝜑 → 𝜒) |
Ref | Expression |
---|---|
elrabd | ⊢ (𝜑 → 𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜓}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elrabd.2 | . 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵) | |
2 | elrabd.3 | . 2 ⊢ (𝜑 → 𝜒) | |
3 | elrabd.1 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒)) | |
4 | 3 | elrab 3677 | . 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜓} ↔ (𝐴 ∈ 𝐵 ∧ 𝜒)) |
5 | 1, 2, 4 | sylanbrc 583 | 1 ⊢ (𝜑 → 𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜓}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1528 ∈ wcel 2105 {crab 3139 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-rab 3144 df-v 3494 |
This theorem is referenced by: nnawordex 8252 ordtypelem7 8976 oemapvali 9135 rankuni2b 9270 harval2 9414 fin23lem11 9727 fin1a2lem11 9820 pinq 10337 negf1o 11058 fiminreOLD 11578 uzind4 12294 zsupss 12325 flval3 13173 serge0 13412 expge0 13453 expge1 13454 hashbclem 13798 rlimrege0 14924 lcmgcdlem 15938 phicl2 16093 hashdvds 16100 phisum 16115 pcpremul 16168 prmreclem1 16240 prmreclem3 16242 prmreclem5 16244 ramub 16337 ramub1lem1 16350 ramub1lem2 16351 prmgaplem3 16377 prmgaplem4 16378 prmgaplem5 16379 prmgaplem6 16380 mrcflem 16865 mrcval 16869 isacs1i 16916 coaval 17316 gsumress 17880 issubmd 17959 mhmeql 17978 ghmeql 18319 pmtrval 18508 pmtrrn 18514 symgsssg 18524 symgfisg 18525 psgnunilem5 18551 pgpssslw 18668 efgsfo 18794 oddvdssubg 18904 dprdwd 19062 lmhmeql 19756 gsumbagdiaglem 20083 psrlidm 20111 psrridm 20112 mplmonmul 20173 coe1fsupp 20310 cofipsgn 20665 frlmssuvc2 20867 dmatmulcl 21037 fctop 21540 cctop 21542 ppttop 21543 pptbas 21544 epttop 21545 ordthauslem 21919 cmpsublem 21935 locfincmp 22062 xkoopn 22125 pthaus 22174 txkgen 22188 xkohaus 22189 xkococnlem 22195 nrmr0reg 22285 fbssfi 22373 filssufilg 22447 uffixsn 22461 ufinffr 22465 ufilen 22466 supnfcls 22556 flimfnfcls 22564 alexsubALTlem4 22586 tmdgsum2 22632 symgtgp 22637 ghmcnp 22650 lmle 23831 iundisj 24076 opnmbllem 24129 vitalilem2 24137 aannenlem2 24845 aalioulem2 24849 radcnv0 24931 jensen 25493 ftalem4 25580 ftalem5 25581 efnnfsumcl 25607 efchtdvds 25663 sqff1o 25686 fsumdvdsdiaglem 25687 dvdsppwf1o 25690 dvdsflf1o 25691 muinv 25697 dchrfi 25758 lgsne0 25838 2lgslem1b 25895 upgr1elem 26824 subumgredg2 26994 subupgr 26996 upgrreslem 27013 umgrreslem 27014 1hevtxdg1 27215 umgr2v2e 27234 tocycfv 30678 cycpm3cl2 30705 fmla1 32531 fnwe2lem2 39529 fnwe2lem3 39530 supminfrnmpt 41595 supminfxr 41616 supminfxr2 41621 supminfxrrnmpt 41623 smflimsuplem5 42975 rabsubmgmd 43935 |
Copyright terms: Public domain | W3C validator |